---

Step * 1 2 of Lemma union-ss_wf


1. ss1 : SeparationSpace
2. ss2 : SeparationSpace
3. y1 : Point(ss2)
4. y2 : Point(ss2)
5. y : Point(ss2)
6. sep : y1 # y2
⊢ ss2."#or" y1 y2 y sep ∈ y1 # y ∨ y2 # y
BY
{ ((Assert ss2 ∈ SeparationSpace BY Auto) THEN D 2 THEN All (Folds ``ss-sep ss-point``) THEN Auto) }

---

Latex:

---

Latex:

1.  ss1  :  SeparationSpace
2.  ss2  :  SeparationSpace
3.  y1  :  Point(ss2)
4.  y2  :  Point(ss2)
5.  y  :  Point(ss2)
6.  sep  :  y1  \#  y2
\mvdash{}  ss2."\#or"  y1  y2  y  sep  \mmember{}  y1  \#  y  \mvee{}  y2  \#  y


By

---

Latex:
((Assert  ss2  \mmember{}  SeparationSpace  BY  Auto)  THEN  D  2  THEN  All  (Folds  ``ss-sep  ss-point``)  THEN  Auto)

---

Home Index