df-e - brismu bridi

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

Definition df-e 147

Description: Definition of {.e} in terms of {ge}. Forethought version of example 12.2-5 from [CLL] p. 14.

**Assertion**
Ref	Expression
df-e	⊢ go ko'a .e ko'e bo'a gi ge ko'a bo'a gi ko'e bo'a

This definition is referenced by: ei 148 eri 149 e-com 150