---

Step * of Lemma dM-point

∀[I:Top]
  (Point(dM(I)) ~ {ac:fset(fset(names(I) + names(I)))| 
                   ↑fset-antichain(union-deq(names(I);names(I);NamesDeq;NamesDeq);ac)} )
BY
{ (Unfold `dM` 0
   THEN (RWO "free-dma-point" 0 THENA Auto)
   THEN Unfold `free-DeMorgan-lattice` 0
   THEN RWO "free-dl-point" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:Top]
    (Point(dM(I))  \msim{}  \{ac:fset(fset(names(I)  +  names(I)))| 
                                      \muparrow{}fset-antichain(union-deq(names(I);names(I);NamesDeq;NamesDeq);ac)\}  )


By

---

Latex:
(Unfold  `dM`  0
  THEN  (RWO  "free-dma-point"  0  THENA  Auto)
  THEN  Unfold  `free-DeMorgan-lattice`  0
  THEN  RWO  "free-dl-point"  0
  THEN  Auto)

---

Home Index