---

Step * 1 of Lemma ss-mem-open-and


1. [X] : SeparationSpace
2. A : Open(X)@i'
3. B : Open(X)@i'
4. x : Point(X)@i
5. B1 : ss-basic(X)@i
6. A B1
7. x ∈ B1
8. B2 : ss-basic(X)@i
9. B B2
10. x ∈ B2
11. ∃u,v:ss-basic(X). ((A u) ∧ (B v) ∧ (ss-basic-and(B1;B2) = ss-basic-and(u;v) ∈ ss-basic(X)))
⊢ x ∈ ss-basic-and(B1;B2)
BY
{ (RWO "ss-mem-basic-and" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [X]  :  SeparationSpace
2.  A  :  Open(X)@i'
3.  B  :  Open(X)@i'
4.  x  :  Point(X)@i
5.  B1  :  ss-basic(X)@i
6.  A  B1
7.  x  \mmember{}  B1
8.  B2  :  ss-basic(X)@i
9.  B  B2
10.  x  \mmember{}  B2
11.  \mexists{}u,v:ss-basic(X).  ((A  u)  \mwedge{}  (B  v)  \mwedge{}  (ss-basic-and(B1;B2)  =  ss-basic-and(u;v)))
\mvdash{}  x  \mmember{}  ss-basic-and(B1;B2)


By

---

Latex:
(RWO  "ss-mem-basic-and"  0  THEN  Auto)

---

Home Index