Step * of Lemma ocmon_connex

g:OCMon. ∀x,y:|g|.  ((↑(x ≤b y)) ∨ (↑(y ≤b x)))
BY
((ProvePropertyLemma `connex` 1) THEN Auto) }


Latex:


Latex:
\mforall{}g:OCMon.  \mforall{}x,y:|g|.    ((\muparrow{}(x  \mleq{}\msubb{}  y))  \mvee{}  (\muparrow{}(y  \mleq{}\msubb{}  x)))


By


Latex:
((ProvePropertyLemma  `connex`  1)  THEN  Auto)




Home Index