:: TSP_1 semantic presentation

K92() is Element of K19(K88())
K88() is set
K19(K88()) is non empty set
K87() is set
K19(K87()) is non empty set
K19(K92()) is non empty set
2 is non empty set
K20(2,2) is non empty set
K20(K20(2,2),2) is non empty set
K19(K20(K20(2,2),2)) is non empty set
K247() is TopStruct
the carrier of K247() is set
{} is empty trivial set
1 is non empty set
X is TopStruct
the carrier of X is set
K19( the carrier of X) is non empty set
A0 is TopStruct
the carrier of A0 is set
K19( the carrier of A0) is non empty set
[#] A0 is non proper Element of K19( the carrier of A0)
[#] X is non proper Element of K19( the carrier of X)
X0 is Element of K19( the carrier of A0)
the topology of A0 is Element of K19(K19( the carrier of A0))
K19(K19( the carrier of A0)) is non empty set
the topology of X is Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
X0 is Element of K19( the carrier of X)
X0 /\ ([#] A0) is Element of K19( the carrier of A0)
c₅ is Element of K19( the carrier of X)
c₅ /\ the carrier of A0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
X0 /\ the carrier of A0 is Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of X)
the topology of X is Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
c₅ /\ ([#] A0) is Element of K19( the carrier of A0)
the topology of A0 is Element of K19(K19( the carrier of A0))
K19(K19( the carrier of A0)) is non empty set
c₅ is Element of K19( the carrier of X)
c₅ /\ ([#] A0) is Element of K19( the carrier of A0)
the topology of A0 is Element of K19(K19( the carrier of A0))
K19(K19( the carrier of A0)) is non empty set
the topology of X is Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
X0 is Element of K19( the carrier of A0)
c₅ is Element of K19( the carrier of A0)
x is Element of K19( the carrier of X)
x /\ the carrier of A0 is Element of K19( the carrier of X)
x /\ ([#] A0) is Element of K19( the carrier of A0)
c₅ is Element of K19( the carrier of X)
c₅ /\ ([#] A0) is Element of K19( the carrier of A0)
x is Element of K19( the carrier of X)
y is Element of K19( the carrier of X)
y /\ the carrier of A0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of A0)
y is Element of K19( the carrier of X)
y /\ the carrier of A0 is Element of K19( the carrier of X)
X is TopStruct
the carrier of X is set
K19( the carrier of X) is non empty set
A0 is SubSpace of X
the carrier of A0 is set
K19( the carrier of A0) is non empty set
X0 is Element of K19( the carrier of X)
X0 /\ the carrier of A0 is Element of K19( the carrier of X)
[#] A0 is non proper Element of K19( the carrier of A0)
[#] X is non proper Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
X0 /\ X0 is Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of A0)
X is TopStruct
the carrier of X is set
K19( the carrier of X) is non empty set
A0 is TopStruct
the carrier of A0 is set
K19( the carrier of A0) is non empty set
[#] A0 is non proper Element of K19( the carrier of A0)
[#] X is non proper Element of K19( the carrier of X)
([#] A0) \ ([#] X) is Element of K19( the carrier of A0)
X0 is Element of K19( the carrier of A0)
([#] A0) \ X0 is Element of K19( the carrier of A0)
c₅ is Element of K19( the carrier of X)
c₅ /\ the carrier of A0 is Element of K19( the carrier of X)
([#] X) \ c₅ is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x /\ the carrier of A0 is Element of K19( the carrier of X)
([#] X) \ x is Element of K19( the carrier of X)
([#] A0) \ (c₅ /\ the carrier of A0) is Element of K19( the carrier of A0)
([#] A0) \ c₅ is Element of K19( the carrier of A0)
([#] A0) \ the carrier of A0 is Element of K19( the carrier of A0)
(([#] A0) \ c₅) \/ (([#] A0) \ the carrier of A0) is Element of K19( the carrier of A0)
(([#] A0) \ c₅) \/ {} is set
([#] A0) /\ x is Element of K19( the carrier of X)
(([#] A0) \ ([#] X)) \/ (([#] A0) /\ x) is set
c₅ is Element of K19( the carrier of X)
c₅ /\ the carrier of A0 is Element of K19( the carrier of X)
([#] X) \ c₅ is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
([#] X) \ x is Element of K19( the carrier of X)
([#] A0) \ c₅ is Element of K19( the carrier of A0)
([#] A0) \ the carrier of A0 is Element of K19( the carrier of A0)
(([#] A0) \ c₅) \/ (([#] A0) \ the carrier of A0) is Element of K19( the carrier of A0)
(([#] A0) \ c₅) \/ {} is set
([#] A0) /\ x is Element of K19( the carrier of X)
(([#] A0) \ ([#] X)) \/ (([#] A0) /\ x) is set
x /\ the carrier of A0 is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x /\ the carrier of A0 is Element of K19( the carrier of X)
([#] A0) \ ([#] X) is Element of K19( the carrier of A0)
X0 is Element of K19( the carrier of A0)
([#] A0) \ X0 is Element of K19( the carrier of A0)
([#] A0) \ (([#] A0) \ X0) is Element of K19( the carrier of A0)
x is Element of K19( the carrier of X)
x /\ the carrier of A0 is Element of K19( the carrier of X)
([#] X) \ x is Element of K19( the carrier of X)
y is Element of K19( the carrier of X)
y /\ the carrier of A0 is Element of K19( the carrier of X)
([#] X) \ y is Element of K19( the carrier of X)
([#] A0) \ x is Element of K19( the carrier of A0)
([#] A0) \ the carrier of A0 is Element of K19( the carrier of A0)
(([#] A0) \ x) \/ (([#] A0) \ the carrier of A0) is Element of K19( the carrier of A0)
(([#] A0) \ x) \/ {} is set
([#] A0) /\ y is Element of K19( the carrier of X)
(([#] A0) \ ([#] X)) \/ (([#] A0) /\ y) is set
c₅ is Element of K19( the carrier of X)
c₅ /\ the carrier of A0 is Element of K19( the carrier of X)
([#] X) \ c₅ is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
([#] X) \ x is Element of K19( the carrier of X)
([#] A0) \ c₅ is Element of K19( the carrier of A0)
([#] A0) \ the carrier of A0 is Element of K19( the carrier of A0)
(([#] A0) \ c₅) \/ (([#] A0) \ the carrier of A0) is Element of K19( the carrier of A0)
(([#] A0) \ c₅) \/ {} is set
([#] A0) /\ x is Element of K19( the carrier of X)
(([#] A0) \ ([#] X)) \/ (([#] A0) /\ x) is set
x /\ the carrier of A0 is Element of K19( the carrier of X)
([#] A0) \ (([#] A0) \ X0) is Element of K19( the carrier of A0)
x is Element of K19( the carrier of X)
x /\ the carrier of A0 is Element of K19( the carrier of X)
X is TopStruct
the carrier of X is set
K19( the carrier of X) is non empty set
A0 is SubSpace of X
the carrier of A0 is set
K19( the carrier of A0) is non empty set
X0 is Element of K19( the carrier of X)
X0 /\ the carrier of A0 is Element of K19( the carrier of X)
[#] A0 is non proper Element of K19( the carrier of A0)
[#] X is non proper Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
X0 /\ X0 is Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of A0)
X is TopStruct
the carrier of X is set
K19( the carrier of X) is non empty set
A0 is Element of the carrier of X
X0 is Element of the carrier of X
X0 is Element of K19( the carrier of X)
A0 is Element of the carrier of X
X0 is Element of the carrier of X
X0 is Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of X)
X is TopStruct
the carrier of X is set
K19( the carrier of X) is non empty set
A0 is Element of the carrier of X
X0 is Element of the carrier of X
X0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
X0 ` is Element of K19( the carrier of X)
the carrier of X \ X0 is set
[#] X is non proper Element of K19( the carrier of X)
c<sub>5</sub> is Element of K19( the carrier of X)
([#] X) \ c<sub>5</sub> is Element of K19( the carrier of X)
c<sub>5</sub> is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
X0 ` is Element of K19( the carrier of X)
the carrier of X \ X0 is set
[#] X is non proper Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of X)
([#] X) \ c₅ is Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of X)
A0 is Element of the carrier of X
X0 is Element of the carrier of X
X0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
X0 ` is Element of K19( the carrier of X)
the carrier of X \ X0 is set
c<sub>5</sub> is Element of K19( the carrier of X)
[#] X is non proper Element of K19( the carrier of X)
([#] X) \ X0 is Element of K19( the carrier of X)
c<sub>5</sub> is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
X0 ` is Element of K19( the carrier of X)
the carrier of X \ X0 is set
c₅ is Element of K19( the carrier of X)
[#] X is non proper Element of K19( the carrier of X)
([#] X) \ X0 is Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of X)
X is non empty TopStruct
the carrier of X is non empty set
A0 is Element of the carrier of X
{A0} is non empty trivial Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
X0 is Element of the carrier of X
X0 is Element of the carrier of X
X is non empty non trivial TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
the carrier of X is non empty non trivial set
A0 is Element of the carrier of X
X0 is Element of the carrier of X
X0 is Element of the carrier of X
c₅ is Element of the carrier of X
K19( the carrier of X) is non empty set
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
y is Element of K19( the carrier of X)
A0 is Element of the carrier of X
X0 is Element of the carrier of X
the non empty trivial V47() V52(1) strict TopSpace-like T_0 discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct is non empty trivial V47() V52(1) strict TopSpace-like T_0 discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
the non empty non trivial strict TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct is non empty non trivial strict TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
A0 is Element of the carrier of X
X0 is Element of the carrier of X
K19( the carrier of X) is non empty set
{A0} is non empty trivial Element of K19( the carrier of X)
X0 is non empty trivial Element of K19( the carrier of X)
X0 is non empty trivial Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
A0 is Element of the carrier of X
{A0} is non empty trivial Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Cl {A0} is closed Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
A0 is Element of the carrier of X
X0 is Element of the carrier of X
K19( the carrier of X) is non empty set
X0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
{A0} is non empty trivial Element of K19( the carrier of X)
Cl {A0} is closed Element of K19( the carrier of X)
(Cl {A0}) /\ X0 is Element of K19( the carrier of X)
X0 ` is Element of K19( the carrier of X)
the carrier of X \ X0 is set
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
X0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
(Cl {X0}) /\ X0 is Element of K19( the carrier of X)
X0 ` is Element of K19( the carrier of X)
the carrier of X \ X0 is set
{A0} is non empty trivial Element of K19( the carrier of X)
Cl {A0} is closed Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
{A0} is non empty trivial Element of K19( the carrier of X)
Cl {A0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{A0} is non empty trivial Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Cl {A0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
A0 is Element of the carrier of X
X0 is Element of the carrier of X
K19( the carrier of X) is non empty set
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{A0} is non empty trivial Element of K19( the carrier of X)
Cl {A0} is closed Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
A0 is Element of the carrier of X
X0 is Element of the carrier of X
{X0} is non empty trivial Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Cl {X0} is closed Element of K19( the carrier of X)
{A0} is non empty trivial Element of K19( the carrier of X)
Cl {A0} is closed Element of K19( the carrier of X)
A0 is Element of the carrier of X
X0 is Element of the carrier of X
{A0} is non empty trivial Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Cl {A0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
A0 is Element of the carrier of X
X0 is Element of the carrier of X
{X0} is non empty trivial Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Cl {X0} is closed Element of K19( the carrier of X)
{A0} is non empty trivial Element of K19( the carrier of X)
Cl {A0} is closed Element of K19( the carrier of X)
A0 is Element of the carrier of X
X0 is Element of the carrier of X
{X0} is non empty trivial Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Cl {X0} is closed Element of K19( the carrier of X)
{A0} is non empty trivial Element of K19( the carrier of X)
Cl {A0} is closed Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is Element of K19( the carrier of X)
X0 is Element of the carrier of X
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
X0 is set
c₅ is Element of the carrier of X
{c₅} is non empty trivial Element of K19( the carrier of X)
Cl {c₅} is closed Element of K19( the carrier of X)
(Cl {c₅}) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl {c<sub>5</sub>}) is set
X is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
the non empty non trivial strict TopSpace-like T_0 discrete non anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct is non empty non trivial strict TopSpace-like T_0 discrete non anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
the non empty non trivial strict TopSpace-like non T_0 non discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct is non empty non trivial strict TopSpace-like non T_0 non discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
X is TopStruct
the carrier of X is set
K19( the carrier of X) is non empty set
X is non empty TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is Element of K19( the carrier of X)
X0 is Element of the carrier of X
X0 is Element of the carrier of X
c<sub>5</sub> is Element of K19( the carrier of X)
c<sub>5</sub> is Element of K19( the carrier of X)
c<sub>5</sub> ` is Element of K19( the carrier of X)
the carrier of X \ c₅ is set
[#] X is non empty non proper Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
([#] X) \ x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of X)
c₅ ` is Element of K19( the carrier of X)
the carrier of X \ c<sub>5</sub> is set
[#] X is non empty non proper Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
([#] X) \ x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
X0 is Element of the carrier of X
X0 is Element of the carrier of X
c<sub>5</sub> is Element of K19( the carrier of X)
c<sub>5</sub> is Element of K19( the carrier of X)
c<sub>5</sub> ` is Element of K19( the carrier of X)
the carrier of X \ c₅ is set
x is Element of K19( the carrier of X)
[#] X is non empty non proper Element of K19( the carrier of X)
([#] X) \ c₅ is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of X)
c₅ ` is Element of K19( the carrier of X)
the carrier of X \ c<sub>5</sub> is set
x is Element of K19( the carrier of X)
[#] X is non empty non proper Element of K19( the carrier of X)
([#] X) \ c<sub>5</sub> is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
X is TopStruct
the carrier of X is set
K19( the carrier of X) is non empty set
A0 is TopStruct
the carrier of A0 is set
K19( the carrier of A0) is non empty set
the topology of X is Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
TopStruct(# the carrier of X, the topology of X #) is strict TopStruct
the topology of A0 is Element of K19(K19( the carrier of A0))
K19(K19( the carrier of A0)) is non empty set
TopStruct(# the carrier of A0, the topology of A0 #) is strict TopStruct
X0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of A0)
c<sub>5</sub> is Element of the carrier of A0
x is Element of the carrier of A0
y is Element of the carrier of X
F is Element of the carrier of X
F0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of A0)
W1 is Element of K19( the carrier of A0)
W1 is Element of K19( the carrier of A0)
y is Element of the carrier of X
F is Element of the carrier of X
F0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of A0)
W1 is Element of K19( the carrier of A0)
W1 is Element of K19( the carrier of A0)
y is Element of the carrier of X
F is Element of the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is Element of K19( the carrier of X)
X0 is Element of the carrier of X
X0 is Element of the carrier of X
X0 is Element of the carrier of X
X0 is Element of the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
X0 is Element of K19( the carrier of X)
A0 is Element of K19( the carrier of X)
X0 is Element of the carrier of X
c<sub>5</sub> is Element of the carrier of X
X is non empty TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
A0 /\ X0 is Element of K19( the carrier of X)
X is non empty TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
A0 \/ X0 is Element of K19( the carrier of X)
X0 is Element of the carrier of X
c<sub>5</sub> is Element of the carrier of X
A0 \ X0 is Element of K19( the carrier of X)
(A0 \ X0) \/ X0 is Element of K19( the carrier of X)
X0 \ A0 is Element of K19( the carrier of X)
A0 \/ (X0 \ A0) is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
y is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
y is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
y is Element of K19( the carrier of X)
X is non empty TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is Element of K19( the carrier of X)
X0 is Element of K19( the carrier of X)
A0 \/ X0 is Element of K19( the carrier of X)
X0 is Element of the carrier of X
c<sub>5</sub> is Element of the carrier of X
A0 \ X0 is Element of K19( the carrier of X)
(A0 \ X0) \/ X0 is Element of K19( the carrier of X)
X0 \ A0 is Element of K19( the carrier of X)
A0 \/ (X0 \ A0) is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
y is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
y is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
y is Element of K19( the carrier of X)
X is non empty TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is Element of K19( the carrier of X)
X0 is Element of the carrier of X
X0 is Element of the carrier of X
{X0} is non empty trivial Element of K19( the carrier of X)
c<sub>5</sub> is Element of K19( the carrier of X)
A0 /\ c<sub>5</sub> is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
X is non empty TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is non empty Element of K19( the carrier of X)
X0 is set
X0 is Element of A0
{X0} is non empty trivial Element of K19(A0)
K19(A0) is non empty set
c<sub>5</sub> is set
x is Element of the carrier of X
y is Element of the carrier of X
F is Element of K19( the carrier of X)
F is Element of K19( the carrier of X)
x is Element of the carrier of X
y is Element of the carrier of X
F is Element of K19( the carrier of X)
F is Element of K19( the carrier of X)
x is Element of the carrier of X
y is Element of the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is Element of K19( the carrier of X)
X0 is Element of the carrier of X
X0 is Element of the carrier of X
c<sub>5</sub> is Element of K19( the carrier of X)
c<sub>5</sub> is Element of K19( the carrier of X)
c<sub>5</sub> ` is Element of K19( the carrier of X)
the carrier of X \ c₅ is set
{X0} is non empty trivial Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of X)
c₅ is Element of K19( the carrier of X)
c₅ ` is Element of K19( the carrier of X)
the carrier of X \ c₅ is set
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
X0 is Element of the carrier of X
X0 is Element of the carrier of X
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is Element of K19( the carrier of X)
X0 is Element of the carrier of X
X0 is Element of the carrier of X
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
X0 is Element of the carrier of X
X0 is Element of the carrier of X
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is Element of K19( the carrier of X)
X0 is Element of the carrier of X
X0 is Element of the carrier of X
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
X0 is Element of the carrier of X
X0 is Element of the carrier of X
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
{X0} is non empty trivial Element of K19( the carrier of X)
Cl {X0} is closed Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is empty trivial proper open Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
A0 is Element of the carrier of X
{A0} is non empty trivial Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
X is non empty TopStruct
the non empty trivial V47() V52(1) strict T_0 SubSpace of X is non empty trivial V47() V52(1) strict T_0 SubSpace of X
X is TopStruct
A0 is SubSpace of X
[#] A0 is non proper Element of K19( the carrier of A0)
the carrier of A0 is set
K19( the carrier of A0) is non empty set
[#] X is non proper Element of K19( the carrier of X)
the carrier of X is set
K19( the carrier of X) is non empty set
X is TopStruct
A0 is SubSpace of X
the carrier of X is set
the carrier of A0 is set
K19( the carrier of X) is non empty set
X0 is Element of the carrier of X
c₅ is Element of the carrier of X
K19( the carrier of A0) is non empty set
x is Element of the carrier of A0
y is Element of the carrier of A0
F is Element of K19( the carrier of A0)
F is Element of K19( the carrier of A0)
X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
F0 /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
F0 /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
K19( the carrier of A0) is non empty set
x is Element of the carrier of A0
y is Element of the carrier of A0
F is Element of K19( the carrier of A0)
F is Element of K19( the carrier of A0)
X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
F0 /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
F0 /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
K19( the carrier of A0) is non empty set
x is Element of the carrier of A0
y is Element of the carrier of A0
F is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
X0 is Element of the carrier of A0
c₅ is Element of the carrier of A0
x is Element of the carrier of X
y is Element of the carrier of X
F is Element of K19( the carrier of X)
F is Element of K19( the carrier of X)
K19( the carrier of A0) is non empty set
X0 is Element of K19( the carrier of X)
F /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of A0)
F0 is Element of K19( the carrier of A0)
F0 is Element of K19( the carrier of A0)
x is Element of the carrier of X
y is Element of the carrier of X
F is Element of K19( the carrier of X)
F is Element of K19( the carrier of X)
K19( the carrier of A0) is non empty set
X0 is Element of K19( the carrier of X)
F /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of A0)
F0 is Element of K19( the carrier of A0)
F0 is Element of K19( the carrier of A0)
x is Element of the carrier of X
y is Element of the carrier of X
K19( the carrier of A0) is non empty set
K19( the carrier of A0) is non empty set
F is Element of K19( the carrier of A0)
F0 is Element of K19( the carrier of A0)
X is TopStruct
A0 is SubSpace of X
the carrier of X is set
the carrier of A0 is set
K19( the carrier of X) is non empty set
X0 is Element of the carrier of X
c₅ is Element of the carrier of X
K19( the carrier of A0) is non empty set
x is Element of the carrier of A0
y is Element of the carrier of A0
F is Element of K19( the carrier of A0)
F is Element of K19( the carrier of A0)
X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
F0 /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
F0 /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
K19( the carrier of A0) is non empty set
x is Element of the carrier of A0
y is Element of the carrier of A0
F is Element of K19( the carrier of A0)
F is Element of K19( the carrier of A0)
X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
F0 /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
F0 /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
K19( the carrier of A0) is non empty set
x is Element of the carrier of A0
y is Element of the carrier of A0
F is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of X)
X0 is Element of the carrier of A0
c₅ is Element of the carrier of A0
x is Element of the carrier of X
y is Element of the carrier of X
F is Element of K19( the carrier of X)
F is Element of K19( the carrier of X)
K19( the carrier of A0) is non empty set
X0 is Element of K19( the carrier of X)
F /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of A0)
F0 is Element of K19( the carrier of A0)
F0 is Element of K19( the carrier of A0)
x is Element of the carrier of X
y is Element of the carrier of X
F is Element of K19( the carrier of X)
F is Element of K19( the carrier of X)
K19( the carrier of A0) is non empty set
X0 is Element of K19( the carrier of X)
F /\ X0 is Element of K19( the carrier of X)
F0 is Element of K19( the carrier of A0)
F0 is Element of K19( the carrier of A0)
F0 is Element of K19( the carrier of A0)
x is Element of the carrier of X
y is Element of the carrier of X
K19( the carrier of A0) is non empty set
K19( the carrier of A0) is non empty set
F is Element of K19( the carrier of A0)
F0 is Element of K19( the carrier of A0)
X is non empty TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is non empty SubSpace of X
the carrier of A0 is non empty set
X0 is Element of K19( the carrier of X)
X0 is Element of the carrier of X
c₅ is Element of the carrier of X
X0 is Element of the carrier of X
c₅ is Element of the carrier of X
X is non empty TopStruct
A0 is non empty SubSpace of X
X0 is non empty T_0 SubSpace of X
the carrier of X is non empty set
K19( the carrier of X) is non empty set
the carrier of X0 is non empty set
the carrier of A0 is non empty set
X0 is non empty Element of K19( the carrier of X)
[#] A0 is non empty non proper Element of K19( the carrier of A0)
K19( the carrier of A0) is non empty set
c₅ is non empty Element of K19( the carrier of X)
[#] X0 is non empty non proper Element of K19( the carrier of X0)
K19( the carrier of X0) is non empty set
X is non empty TopSpace-like TopStruct
A0 is non empty T_0 SubSpace of X
X0 is non empty SubSpace of X
A0 meet X0 is non empty strict SubSpace of X
the carrier of X is non empty set
K19( the carrier of X) is non empty set
the carrier of A0 is non empty set
the carrier of X0 is non empty set
the carrier of (A0 meet X0) is non empty set
X0 is non empty Element of K19( the carrier of X)
c₅ is non empty Element of K19( the carrier of X)
X0 /\ c₅ is Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
A0 is non empty T_0 SubSpace of X
X0 is non empty T_0 SubSpace of X
A0 union X0 is non empty strict SubSpace of X
the carrier of X is non empty set
K19( the carrier of X) is non empty set
the carrier of A0 is non empty set
the carrier of X0 is non empty set
X0 is non empty Element of K19( the carrier of X)
c₅ is non empty Element of K19( the carrier of X)
the carrier of (A0 union X0) is non empty set
X0 \/ c₅ is non empty Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
A0 is non empty T_0 SubSpace of X
X0 is non empty T_0 SubSpace of X
A0 union X0 is non empty strict SubSpace of X
the carrier of X is non empty set
K19( the carrier of X) is non empty set
the carrier of A0 is non empty set
the carrier of X0 is non empty set
X0 is non empty Element of K19( the carrier of X)
c₅ is non empty Element of K19( the carrier of X)
the carrier of (A0 union X0) is non empty set
X0 \/ c₅ is non empty Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A0 is non empty Element of K19( the carrier of X)
X0 is non empty strict SubSpace of X
the carrier of X0 is non empty set
X0 is non empty strict T_0 SubSpace of X
the carrier of X0 is non empty set
X is non empty non trivial TopSpace-like TopStruct
the non empty trivial V47() V52(1) strict T_0 proper SubSpace of X is non empty trivial V47() V52(1) strict T_0 proper SubSpace of X
X is non empty TopSpace-like T_0 TopStruct
A0 is non empty SubSpace of X
the carrier of X is non empty set
K19( the carrier of X) is non empty set
the carrier of A0 is non empty set
X0 is non empty Element of K19( the carrier of X)
X0 is non empty Element of K19( the carrier of X)
X is non empty non trivial TopSpace-like non T_0 non discrete TopStruct
A0 is non empty SubSpace of X
the carrier of X is non empty non trivial set
K19( the carrier of X) is non empty set
the carrier of A0 is non empty set
X0 is non empty Element of K19( the carrier of X)
X0 is non empty Element of K19( the carrier of X)
A0 is non empty SubSpace of X
X is non empty non trivial TopSpace-like non T_0 non discrete TopStruct
the non empty non trivial strict non T_0 closed open non proper SubSpace of X is non empty non trivial strict non T_0 closed open non proper SubSpace of X
X is non empty non trivial TopSpace-like non T_0 non discrete TopStruct
the carrier of X is non empty non trivial set
K19( the carrier of X) is non empty set
A0 is Element of K19( the carrier of X)
X0 is non empty strict SubSpace of X
the carrier of X0 is non empty set
X0 is strict non T_0 SubSpace of X
the carrier of X0 is set