---

Step * of Lemma cal-point

∀[T,eq,P:Top].
  (Point(constrained-antichain-lattice(T;eq;P)) ~ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)} )
BY
{ (Auto THEN RW (AddrC [1] (TagC (mk_tag_term 40))) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,eq,P:Top].
    (Point(constrained-antichain-lattice(T;eq;P))  \msim{}  \{ac:fset(fset(T))| 
                                                                                                      (\muparrow{}fset-antichain(eq;ac))  \mwedge{}  fset-all(ac;a.P  a)\}  )


By

---

Latex:
(Auto  THEN  RW  (AddrC  [1]  (TagC  (mk\_tag\_term  40)))  0  THEN  Auto)

---

Home Index