:: CONNSP_3 semantic presentation

K96() is set

K10(K96()) is non empty set

{} is set

the empty set is empty set

1 is non empty set

union {} is set

T is TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

K10(K10( the carrier of T)) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is Element of K10(K10( the carrier of T))

union X is Element of K10( the carrier of T)

X is Element of K10(K10( the carrier of T))

union X is Element of K10( the carrier of T)

x is Element of K10(K10( the carrier of T))

union x is Element of K10( the carrier of T)

x is Element of K10(K10( the carrier of T))

union x is Element of K10( the carrier of T)

Y is set

X is set

A2 is Element of K10( the carrier of T)

X is set

A2 is Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

K10(K10( the carrier of T)) is non empty set

X is Element of K10(K10( the carrier of T))

union X is Element of K10( the carrier of T)

X is set

meet X is Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

K10(K10( the carrier of T)) is non empty set

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

{} T is empty proper closed connected Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

(T,({} T)) is Element of K10( the carrier of T)

K10(K10( the carrier of T)) is non empty set

A is Element of K10(K10( the carrier of T))

F is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

F is set

X is Element of the carrier of T

Component_of X is non empty connected Element of K10( the carrier of T)

X is set

x is set

X is set

union A is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

{} T is empty proper closed connected Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

K10(K10( the carrier of T)) is non empty set

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

X is set

meet F is Element of K10( the carrier of T)

{} T is empty closed connected Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

K10(K10( the carrier of T)) is non empty set

X is Element of K10(K10( the carrier of T))

union X is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

{} T is empty proper closed connected Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

(T,F) is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

(T,F) is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

(T,F) is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

(T,X) is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

(T,F) is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

(T,(T,A)) is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

(T,F) is Element of K10( the carrier of T)

K10(K10( the carrier of T)) is non empty set

X is Element of K10(K10( the carrier of T))

union X is Element of K10( the carrier of T)

K10(K10( the carrier of T)) is non empty set

X is Element of K10(K10( the carrier of T))

union X is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

(T,F) is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

A \/ F is Element of K10( the carrier of T)

(T,(A \/ F)) is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

F is Element of the carrier of T

Component_of F is non empty connected Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

A \/ F is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

(T,F) is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X /\ X is Element of K10( the carrier of T)

X \/ X is Element of K10( the carrier of T)

(T,X) is Element of K10( the carrier of T)

A /\ F is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

Cl A is Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

(T,F) is Element of K10( the carrier of T)

A /\ F is Element of K10( the carrier of T)

A /\ (T,F) is Element of K10( the carrier of T)

X is Element of the carrier of T

Component_of X is non empty connected Element of K10( the carrier of T)

(T,A) is Element of K10( the carrier of T)

(T,(T,F)) is Element of K10( the carrier of T)

(T,F) /\ F is Element of K10( the carrier of T)

T is TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

K10(K10( the carrier of T)) is non empty set

A is Element of K10(K10( the carrier of T))

F is Element of K10( the carrier of T)

{} T is empty connected Element of K10( the carrier of T)

T is TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

K10(K10( the carrier of T)) is non empty set

{} T is empty connected Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

{} T is empty proper closed connected Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

K10(K10( the carrier of T)) is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

{ b

bool the carrier of T is non empty Element of K10(K10( the carrier of T))

K10(K10( the carrier of T)) is non empty set

F is set

X is Element of K10( the carrier of T)

F is Element of K10(K10( the carrier of T))

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

union F is Element of K10( the carrier of T)

X is set

X is Element of the carrier of T

Component_of X is non empty connected Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of the carrier of T

Component_of F is non empty connected Element of K10( the carrier of T)

K10(K10( the carrier of T)) is non empty set

X is Element of K10(K10( the carrier of T))

union X is Element of K10( the carrier of T)

X is set

x is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

A \/ F is Element of K10( the carrier of T)

A /\ F is Element of K10( the carrier of T)

K10(K10( the carrier of T)) is non empty set

X is Element of K10(K10( the carrier of T))

union X is Element of K10( the carrier of T)

X is Element of K10(K10( the carrier of T))

union X is Element of K10( the carrier of T)

X \/ X is Element of K10(K10( the carrier of T))

x is Element of K10( the carrier of T)

X /\ X is Element of K10(K10( the carrier of T))

x is Element of K10(K10( the carrier of T))

Y is Element of K10( the carrier of T)

union x is Element of K10( the carrier of T)

Y is set

X is set

Y3 is set

B3 is Element of K10( the carrier of T)

A2 is Element of K10( the carrier of T)

X /\ Y3 is set

Y is set

X is set

x is Element of K10(K10( the carrier of T))

union x is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

K10(K10( the carrier of T)) is non empty set

A is Element of K10(K10( the carrier of T))

union A is Element of K10( the carrier of T)

{ b

( b

bool the carrier of T is non empty Element of K10(K10( the carrier of T))

F is set

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

F is Element of K10(K10( the carrier of T))

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

x is Element of K10( the carrier of T)

union F is Element of K10( the carrier of T)

X is set

X is set

x is Element of K10( the carrier of T)

Y is Element of K10(K10( the carrier of T))

union Y is Element of K10( the carrier of T)

X is set

A2 is Element of K10( the carrier of T)

X is set

X is set

x is Element of K10( the carrier of T)

Y is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

K10(K10( the carrier of T)) is non empty set

A is Element of K10(K10( the carrier of T))

meet A is Element of K10( the carrier of T)

{ b

( not b

bool the carrier of T is non empty Element of K10(K10( the carrier of T))

F is set

X is Element of K10( the carrier of T)

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

X is set

X is set

x is Element of K10( the carrier of T)

Y is Element of K10(K10( the carrier of T))

union Y is Element of K10( the carrier of T)

X is set

A2 is Element of K10( the carrier of T)

B3 is Element of K10( the carrier of T)

Y3 is Element of the carrier of T

Component_of Y3 is non empty connected Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is set

X is set

x is Element of K10( the carrier of T)

Y is set

{} T is empty proper closed connected Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

A \ F is Element of K10( the carrier of T)

K10(K10( the carrier of T)) is non empty set

X is Element of K10(K10( the carrier of T))

union X is Element of K10( the carrier of T)

X is Element of K10(K10( the carrier of T))

union X is Element of K10( the carrier of T)

X \ X is Element of K10(K10( the carrier of T))

x is Element of K10(K10( the carrier of T))

union x is Element of K10( the carrier of T)

Y is set

X is set

A2 is Element of K10( the carrier of T)

Y3 is set

B3 is Element of K10( the carrier of T)

A2 /\ B3 is Element of K10( the carrier of T)

Y is Element of K10( the carrier of T)

Y is set

X is set

A2 is Element of K10( the carrier of T)

T is TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

F is Element of the carrier of T

A is Element of K10( the carrier of T)

T | A is strict SubSpace of T

the carrier of (T | A) is set

[#] (T | A) is non proper Element of K10( the carrier of (T | A))

K10( the carrier of (T | A)) is non empty set

T is TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

T | A is strict SubSpace of T

the carrier of (T | A) is set

F is Element of the carrier of (T | A)

T is TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

A /\ F is Element of K10( the carrier of T)

T | F is strict SubSpace of T

the carrier of (T | F) is set

K10( the carrier of (T | F)) is non empty set

[#] (T | F) is non proper Element of K10( the carrier of (T | F))

T is TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

T | A is strict SubSpace of T

the carrier of (T | A) is set

K10( the carrier of (T | A)) is non empty set

F is Element of K10( the carrier of (T | A))

T is TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

F is Element of the carrier of T

A is Element of K10( the carrier of T)

T | A is strict SubSpace of T

the carrier of (T | A) is set

[#] (T | A) is non proper Element of K10( the carrier of (T | A))

K10( the carrier of (T | A)) is non empty set

X is Element of the carrier of (T | A)

Component_of X is Element of K10( the carrier of (T | A))

X is Element of K10( the carrier of T)

x is Element of the carrier of (T | A)

Component_of x is Element of K10( the carrier of (T | A))

[#] (T | A) is non proper Element of K10( the carrier of (T | A))

K10( the carrier of (T | A)) is non empty set

X is Element of K10( the carrier of T)

x is Element of K10( the carrier of T)

X is Element of the carrier of (T | A)

Component_of X is Element of K10( the carrier of (T | A))

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of the carrier of T

(T,A,F) is Element of K10( the carrier of T)

X is non empty Element of K10( the carrier of T)

T | X is non empty strict TopSpace-like SubSpace of T

the carrier of (T | X) is non empty set

X is Element of the carrier of (T | X)

Component_of X is non empty connected Element of K10( the carrier of (T | X))

K10( the carrier of (T | X)) is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

T | A is strict TopSpace-like SubSpace of T

F is Element of the carrier of T

(T,A,F) is Element of K10( the carrier of T)

(T,A,F) is Element of the carrier of (T | A)

the carrier of (T | A) is set

Component_of (T,A,F) is Element of K10( the carrier of (T | A))

K10( the carrier of (T | A)) is non empty set

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

T | F is strict TopSpace-like SubSpace of T

(T,A,F) is Element of K10( the carrier of (T | F))

the carrier of (T | F) is set

K10( the carrier of (T | F)) is non empty set

A /\ F is Element of K10( the carrier of T)

the topology of T is non empty Element of K10(K10( the carrier of T))

K10(K10( the carrier of T)) is non empty set

[#] (T | F) is non proper closed Element of K10( the carrier of (T | F))

A /\ ([#] (T | F)) is Element of K10( the carrier of (T | F))

the topology of (T | F) is non empty Element of K10(K10( the carrier of (T | F)))

K10(K10( the carrier of (T | F))) is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

T | F is strict TopSpace-like SubSpace of T

(T,A,F) is Element of K10( the carrier of (T | F))

the carrier of (T | F) is set

K10( the carrier of (T | F)) is non empty set

A /\ F is Element of K10( the carrier of T)

Cl (T,A,F) is Element of K10( the carrier of (T | F))

Cl A is Element of K10( the carrier of T)

(Cl A) /\ F is Element of K10( the carrier of T)

[#] (T | F) is non proper closed Element of K10( the carrier of (T | F))

(Cl A) /\ ([#] (T | F)) is Element of K10( the carrier of (T | F))

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

T | A is strict TopSpace-like SubSpace of T

the carrier of (T | A) is set

K10( the carrier of (T | A)) is non empty set

F is Element of K10( the carrier of (T | A))

Cl F is Element of K10( the carrier of (T | A))

(T,A,F) is Element of K10( the carrier of T)

Cl (T,A,F) is Element of K10( the carrier of T)

(Cl (T,A,F)) /\ A is Element of K10( the carrier of T)

[#] (T | A) is non proper closed Element of K10( the carrier of (T | A))

(T,(T,A,F),A) is Element of K10( the carrier of (T | A))

(T,A,F) /\ A is Element of K10( the carrier of T)

Cl (T,(T,A,F),A) is Element of K10( the carrier of (T | A))

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

T | F is strict TopSpace-like SubSpace of T

(T,A,F) is Element of K10( the carrier of (T | F))

the carrier of (T | F) is set

K10( the carrier of (T | F)) is non empty set

A /\ F is Element of K10( the carrier of T)

Cl (T,A,F) is Element of K10( the carrier of (T | F))

Cl A is Element of K10( the carrier of T)

(Cl A) /\ F is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

T | A is strict TopSpace-like SubSpace of T

the carrier of (T | A) is set

K10( the carrier of (T | A)) is non empty set

F is Element of K10( the carrier of (T | A))

(T,A,F) is Element of K10( the carrier of T)

(T,(T,A,F),A) is Element of K10( the carrier of (T | A))

(T,A,F) /\ A is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is Element of K10( the carrier of T)

F is Element of the carrier of T

(T,A,F) is Element of K10( the carrier of T)

X is non empty Element of K10( the carrier of T)

T | X is non empty strict TopSpace-like SubSpace of T

(T,X,F) is Element of the carrier of (T | X)

the carrier of (T | X) is non empty set

Component_of (T,X,F) is non empty connected Element of K10( the carrier of (T | X))

K10( the carrier of (T | X)) is non empty set

T | A is strict TopSpace-like SubSpace of T

(T,A,F) is Element of the carrier of (T | A)

the carrier of (T | A) is set

Component_of (T,A,F) is Element of K10( the carrier of (T | A))

K10( the carrier of (T | A)) is non empty set

T is non empty TopSpace-like TopStruct

[#] T is non empty non proper closed Element of K10( the carrier of T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

A is (T)

T is non empty TopSpace-like TopStruct

A is non empty (T)

the carrier of T is non empty set

K10( the carrier of T) is non empty set

K10(K10( the carrier of T)) is non empty set

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

X is set

X is Element of K10( the carrier of T)

{X} is set

x is set

Y is Element of K10( the carrier of T)

x is set