---

Step * 1 of Lemma qoset_lt_irrefl


1. s : QOSet
2. a : |s|
3. b : |s|
4. a <s b
⊢ ¬(a = b ∈ |s|)
BY
{ ((FLemma `set_lt_is_sp_of_leq` [4] 
THENM FLemma `strict_part_irrefl` [5]) THEN Auto) 
 }

---

Latex:

---

Latex:

1.  s  :  QOSet
2.  a  :  |s|
3.  b  :  |s|
4.  a  <s  b
\mvdash{}  \mneg{}(a  =  b)


By

---

Latex:
((FLemma  `set\_lt\_is\_sp\_of\_leq`  [4] 
THENM  FLemma  `strict\_part\_irrefl`  [5])  THEN  Auto) 

---

Home Index