---

Step * 1 1 of Lemma union-ss_wf


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index