:: 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

c

X0 is Element of K19( the carrier of X)

X0 /\ the carrier of A0 is Element of K19( the carrier of X)

c

the topology of X is Element of K19(K19( the carrier of X))

K19(K19( the carrier of X)) is non empty set

c

the topology of A0 is Element of K19(K19( the carrier of A0))

K19(K19( the carrier of A0)) is non empty set

c

c

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

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

c

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

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

c

([#] X) \ c

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

([#] A0) \ c

([#] A0) \ the carrier of A0 is Element of K19( the carrier of A0)

(([#] A0) \ c

(([#] A0) \ c

([#] A0) /\ x is Element of K19( the carrier of X)

(([#] A0) \ ([#] X)) \/ (([#] A0) /\ x) is set

c

c

([#] X) \ c

x is Element of K19( the carrier of X)

([#] X) \ x is Element of K19( the carrier of X)

([#] A0) \ c

([#] A0) \ the carrier of A0 is Element of K19( the carrier of A0)

(([#] A0) \ c

(([#] A0) \ c

([#] 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

c

([#] X) \ c

x is Element of K19( the carrier of X)

([#] X) \ x is Element of K19( the carrier of X)

([#] A0) \ c

([#] A0) \ the carrier of A0 is Element of K19( the carrier of A0)

(([#] A0) \ c

(([#] A0) \ c

([#] 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

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

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

([#] X) \ c

c

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

([#] X) \ c

c

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

[#] X is non proper Element of K19( the carrier of X)

([#] X) \ X0 is Element of K19( the carrier of X)

c

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

[#] X is non proper Element of K19( the carrier of X)

([#] X) \ X0 is Element of K19( the carrier of X)

c

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

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

{c

Cl {c

(Cl {c

the carrier of X \ (Cl {c

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

c

c

the carrier of X \ c

[#] 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

c

c

the carrier of X \ c

[#] 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

c

c

the carrier of X \ c

x is Element of K19( the carrier of X)

[#] X is non empty non proper Element of K19( the carrier of X)

([#] X) \ c

x is Element of K19( the carrier of X)

c

c

c

the carrier of X \ c

x is Element of K19( the carrier of X)

[#] X is non empty non proper Element of K19( the carrier of X)

([#] X) \ c

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

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

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

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

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

A0 /\ c

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

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

c

c

the carrier of X \ c

{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

c

c

the carrier of X \ c

{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

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

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

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

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

X0 is Element of the carrier of X

c

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

[#] 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

X0 /\ c

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

the carrier of (A0 union X0) is non empty set

X0 \/ c

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

the carrier of (A0 union X0) is non empty set

X0 \/ c

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