---

Step * of Lemma set_lt_irreflexivity

∀[s:QOSet]. ∀[a:|s|].  False supposing a <s a
BY
{ ((RepD THENM FLemma `qoset_lt_irrefl` [-1] THENM  
D (-1)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[s:QOSet].  \mforall{}[a:|s|].    False  supposing  a  <s  a


By

---

Latex:
((RepD  THENM  FLemma  `qoset\_lt\_irrefl`  [-1]  THENM   
D  (-1))  THEN  Auto)

---

Home Index