---

Step * of Lemma ocmon_anti_sym

∀[g:OCMon]. ∀[x,y:|g|].  (x = y ∈ |g|) supposing ((↑(y ≤b x)) and (↑(x ≤b y)))
BY
{ ((ProvePropertyLemma `anti_sym` 1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g:OCMon].  \mforall{}[x,y:|g|].    (x  =  y)  supposing  ((\muparrow{}(y  \mleq{}\msubb{}  x))  and  (\muparrow{}(x  \mleq{}\msubb{}  y)))


By

---

Latex:
((ProvePropertyLemma  `anti\_sym`  1)  THEN  Auto)

---

Home Index