---

Step * of Lemma ss-mem-open-or

No Annotations
∀[X:SeparationSpace]. ∀T:Type. ∀F:T ⟶ Open(X). ∀x:Point(X).  (x ∈ ⋃t:T.F[t] ⇐⇒ ∃t:T. x ∈ F[t])
BY
{ (Auto THEN All (RepUR ``ss-mem-open ss-open-or``) THEN ExRepD THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:SeparationSpace].  \mforall{}T:Type.  \mforall{}F:T  {}\mrightarrow{}  Open(X).  \mforall{}x:Point(X).    (x  \mmember{}  \mcup{}t:T.F[t]  \mLeftarrow{}{}\mRightarrow{}  \mexists{}t:T.  x  \mmember{}  F[t])


By

---

Latex:
(Auto  THEN  All  (RepUR  ``ss-mem-open  ss-open-or``)  THEN  ExRepD  THEN  Auto)

---

Home Index