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

---

Definition df-o 198

Description: Definition of {.o} in terms of {go}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14.

Assertion

Ref	Expression
df-o	⊢ go ko'a .o ko'e bo'a gi go ko'a bo'a gi ko'e bo'a

---

This definition is referenced by:  oi  199  ori  200  o-com  201  duis  253  duris  255  kihirduhi-refl  684  kihirnihi-antisym  685

Copyright terms: Public domain

W3C validator