df-ceihi - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > df-ceihi

Definition df-ceihi 207

Description: The predicate which is always true. Note that both sides are relational: the left-hand side definitionally only has one inhabitant, so this definition asserts that {ko'a du ko'a} is only true via one path.

**Assertion**
Ref	Expression
df-ceihi	⊢ go cei'i gi ko'a du ko'a

This definition is referenced by: ceihi 208

W3C validator