:: TEX_4 semantic presentation

K122() is Element of bool K118()

K118() is set

bool K118() is non empty set

K96() is set

bool K96() is non empty set

bool K122() is non empty set

2 is non empty set

[:2,2:] is non empty set

[:[:2,2:],2:] is non empty set

bool [:[:2,2:],2:] is non empty set

K251() is non empty strict TopSpace-like TopStruct

the carrier of K251() is non empty set

{} is empty trivial set

the empty trivial set is empty trivial set

1 is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is empty trivial open closed boundary nowhere_dense Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty non proper Element of bool the carrier of X

Cl X0 is non empty closed Element of bool the carrier of X

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

X is non empty non trivial TopSpace-like TopStruct

the carrier of X is non empty non trivial set

bool the carrier of X is non empty set

X0 is non empty non trivial Element of bool the carrier of X

Cl X0 is non empty closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

{ b

meet { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

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

D is set

A1 is Element of bool the carrier of X

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

A1 is set

D is non empty Element of bool (bool the carrier of X)

A2 is Element of bool the carrier of X

meet D is Element of bool the carrier of X

A1 is Element of bool the carrier of X

A2 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

Cl {X0} is non empty closed Element of bool the carrier of X

{ b

meet { b

{ b

A1 is set

A2 is Element of bool the carrier of X

A1 is set

A2 is Element of bool the carrier of X

meet { b

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty non proper Element of bool the carrier of X

Int X0 is open Element of bool the carrier of X

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is proper Element of bool the carrier of X

Int X0 is open Element of bool the carrier of X

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is empty trivial proper open closed boundary nowhere_dense Element of bool the carrier of X

Int X0 is empty trivial proper open closed boundary nowhere_dense Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Int X0 is open Element of bool the carrier of X

{ b

union { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

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

D is set

A1 is Element of bool the carrier of X

{} X is empty trivial proper open closed boundary nowhere_dense Element of bool the carrier of X

A1 is set

D is non empty Element of bool (bool the carrier of X)

A2 is Element of bool the carrier of X

union D is Element of bool the carrier of X

A1 is Element of bool the carrier of X

A2 is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

[#] X is non empty non proper dense Element of bool the carrier of X

D is Element of bool the carrier of X

([#] X) \ D is Element of bool the carrier of X

X0 \ D is Element of bool the carrier of X

A is Element of the carrier of X

A2 is set

(([#] X) \ D) ` is Element of bool the carrier of X

the carrier of X \ (([#] X) \ D) is set

D ` is Element of bool the carrier of X

the carrier of X \ D is set

(D `) ` is Element of bool the carrier of X

the carrier of X \ (D `) is set

X0 /\ D is Element of bool the carrier of X

D is Element of bool the carrier of X

([#] X) \ D is Element of bool the carrier of X

X0 \ D is Element of bool the carrier of X

([#] X) \ (([#] X) \ D) is Element of bool the carrier of X

A is Element of the carrier of X

A2 is set

D ` is Element of bool the carrier of X

the carrier of X \ D is set

(([#] X) \ D) ` is Element of bool the carrier of X

the carrier of X \ (([#] X) \ D) is set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of bool the carrier of X

X0 /\ A is Element of bool the carrier of X

D is set

A1 is Element of the carrier of X

D is Element of bool the carrier of X

A is Element of the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of bool the carrier of X

[#] X is non proper dense Element of bool the carrier of X

([#] X) \ A is Element of bool the carrier of X

A ` is Element of bool the carrier of X

the carrier of X \ A is set

(A `) ` is Element of bool the carrier of X

the carrier of X \ (A `) is set

A is Element of bool the carrier of X

([#] X) \ A is Element of bool the carrier of X

([#] X) \ (([#] X) \ A) is Element of bool the carrier of X

A ` is Element of bool the carrier of X

the carrier of X \ A is set

(A `) ` is Element of bool the carrier of X

the carrier of X \ (A `) is set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is TopStruct

the carrier of X0 is set

bool the carrier of X0 is non empty set

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

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

TopStruct(# the carrier of X, the topology of X #) is strict TopStruct

the topology of X0 is Element of bool (bool the carrier of X0)

bool (bool the carrier of X0) is non empty set

TopStruct(# the carrier of X0, the topology of X0 #) is strict TopStruct

A is Element of bool the carrier of X

D is Element of bool the carrier of X0

A1 is Element of bool the carrier of X0

A2 is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

A is Element of bool the carrier of X

X0 is Element of bool the carrier of X

D is Element of bool the carrier of X

A /\ D is Element of bool the carrier of X

X0 /\ D is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial Element of bool the carrier of X

bool the carrier of X is non empty set

A is Element of bool the carrier of X

{X0} /\ A is Element of bool the carrier of X

D is set

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is empty trivial proper boundary Element of bool the carrier of X

A is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

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

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

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

X0 is Element of bool (bool the carrier of X)

meet X0 is Element of bool the carrier of X

union X0 is Element of bool the carrier of X

A is Element of bool the carrier of X

D is set

A1 is Element of bool the carrier of X

A2 is set

A1 is Element of bool the carrier of X

A1 /\ A is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

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

X0 is Element of bool (bool the carrier of X)

meet X0 is Element of bool the carrier of X

union X0 is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

{ b

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

bool the carrier of X is non empty Element of bool (bool the carrier of X)

D is set

A1 is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

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

{ b

{X0} is non empty trivial Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

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

{ b

A is Element of bool the carrier of X

D is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

meet (X,X0) is Element of bool the carrier of X

A is set

D is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

meet (X,X0) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

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

{ b

union (X,X0) is Element of bool the carrier of X

{X0} is non empty trivial Element of bool the carrier of X

meet (X,X0) is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is TopStruct

the carrier of X0 is set

bool the carrier of X0 is non empty set

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

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

TopStruct(# the carrier of X, the topology of X #) is strict TopStruct

the topology of X0 is Element of bool (bool the carrier of X0)

bool (bool the carrier of X0) is non empty set

TopStruct(# the carrier of X0, the topology of X0 #) is strict TopStruct

A is Element of bool the carrier of X

D is Element of bool the carrier of X0

A1 is Element of bool the carrier of X0

A2 is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is set

D is empty trivial proper boundary Element of bool the carrier of X

A is Element of the carrier of X

{A} is non empty trivial Element of bool the carrier of X

A1 is non empty trivial Element of bool the carrier of X

A1 is non empty trivial Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty Element of bool the carrier of X

A is Element of bool the carrier of X

A /\ X0 is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty Element of bool the carrier of X

A is Element of bool the carrier of X

A /\ X0 is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

X0 is Element of the carrier of X

(X,X0) is Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

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

{ b

union (X,X0) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{X0} is non empty trivial Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool the carrier of X

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

A is Element of bool the carrier of X

{X0} is non empty trivial Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

A is Element of the carrier of X

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A) is Element of bool the carrier of X

{A} is non empty trivial Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A) is Element of bool the carrier of X

(X,X0) /\ (X,A) is Element of bool the carrier of X

D is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A1) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A) is Element of bool the carrier of X

{A} is non empty trivial Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A) is Element of bool the carrier of X

{A} is non empty trivial Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{ b

meet { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

D is set

A1 is Element of bool the carrier of X

A1 is set

D is Element of bool (bool the carrier of X)

A2 is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{ b

meet { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

D is set

A1 is Element of bool the carrier of X

A1 is set

D is Element of bool (bool the carrier of X)

A2 is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is set

D is Element of the carrier of X

(X,D) is non empty Element of bool the carrier of X

(X,D) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,D) is Element of bool the carrier of X

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A) is Element of bool the carrier of X

D is Element of the carrier of X

(X,D) is non empty Element of bool the carrier of X

(X,D) is non empty Element of bool (bool the carrier of X)

{ b

union (X,D) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty Element of bool the carrier of X

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A) is Element of bool the carrier of X

A is set

D is Element of the carrier of X

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A1) is Element of bool the carrier of X

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A1) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

{ (X,b

union { (X,b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

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

D is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A1) is Element of bool the carrier of X

D is Element of bool (bool the carrier of X)

union D is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{X0} is non empty trivial Element of bool the carrier of X

(X,{X0}) is Element of bool the carrier of X

{ (X,b

union { (X,b

D is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A1) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A) is Element of bool the carrier of X

(X,A) /\ (X,X0) is Element of bool the carrier of X

A1 is set

A2 is Element of the carrier of X

A1 is set

(X,A2) is non empty Element of bool the carrier of X

(X,A2) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A2) is Element of bool the carrier of X

R is Element of the carrier of X

(X,R) is non empty Element of bool the carrier of X

(X,R) is non empty Element of bool (bool the carrier of X)

{ b

union (X,R) is Element of bool the carrier of X

{R} is non empty trivial Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A) is Element of bool the carrier of X

(X,A) /\ X0 is Element of bool the carrier of X

A1 is set

A2 is Element of the carrier of X

{A2} is non empty trivial Element of bool the carrier of X

{ (X,b

R is set

c

(X,c

(X,c

{ b

union (X,c

(X,{A2}) is Element of bool the carrier of X

union { (X,b

(X,A2) is non empty Element of bool the carrier of X

(X,A2) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A2) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,A) is Element of bool the carrier of X

{ (X,b

union { (X,b

A2 is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A1) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

A is set

D is Element of the carrier of X

{D} is non empty trivial Element of bool the carrier of X

(X,{D}) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,D) is non empty Element of bool the carrier of X

(X,D) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,D) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,(X,X0)) is Element of bool the carrier of X

{ (X,b

union { (X,b

A is set

D is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A1) is Element of bool the carrier of X

A2 is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A1) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of bool the carrier of X

(X,A) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,(X,A)) is Element of bool the carrier of X

{ (X,b

union { (X,b

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

A is Element of bool the carrier of X

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,A) is Element of bool the carrier of X

{ (X,b

union { (X,b

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of bool the carrier of X

X0 \/ A is Element of bool the carrier of X

(X,(X0 \/ A)) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,A) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,X0) \/ (X,A) is Element of bool the carrier of X

D is set

A1 is set

A2 is Element of the carrier of X

(X,A2) is non empty Element of bool the carrier of X

(X,A2) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A2) is Element of bool the carrier of X

A1 is set

A1 is set

A1 is set

A1 is set

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of bool the carrier of X

X0 /\ A is Element of bool the carrier of X

(X,(X0 /\ A)) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,A) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,X0) /\ (X,A) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is empty trivial proper boundary Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

A is set

D is Element of the carrier of X

A1 is set

A2 is Element of the carrier of X

(X,A2) is non empty Element of bool the carrier of X

(X,A2) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A2) is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty non proper Element of bool the carrier of X

(X,X0) is non empty Element of bool the carrier of X

{ (X,b

union { (X,b

X is non empty non trivial TopStruct

the carrier of X is non empty non trivial set

bool the carrier of X is non empty set

X0 is non empty non trivial Element of bool the carrier of X

(X,X0) is non empty Element of bool the carrier of X

{ (X,b

union { (X,b

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of bool the carrier of X

(X,A) is Element of bool the carrier of X

{ (X,b

union { (X,b

D is set

A1 is Element of the carrier of X

A2 is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A1) is Element of bool the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A1) is Element of bool the carrier of X

{A1} is non empty trivial Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

{ b

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

meet { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

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

D is set

A1 is Element of bool the carrier of X

A1 is set

D is Element of bool (bool the carrier of X)

A2 is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of bool the carrier of X

(X,A) is Element of bool the carrier of X

{ (X,b

union { (X,b

D is set

A1 is Element of the carrier of X

A2 is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A1) is Element of bool the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A1) is Element of bool the carrier of X

{A1} is non empty trivial Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

{ b

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

meet { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

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

D is set

A1 is Element of bool the carrier of X

A1 is set

D is Element of bool (bool the carrier of X)

A2 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

A is Element of bool the carrier of X

X0 /\ A is Element of bool the carrier of X

D is set

A1 is Element of the carrier of X

{A1} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A1} is non empty closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

A is Element of the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

A is Element of the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of the carrier of X

D is Element of the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

{D} is non empty trivial V170(X) Element of bool the carrier of X

Cl {D} is non empty closed Element of bool the carrier of X

A is Element of the carrier of X

D is set

A1 is Element of the carrier of X

{A1} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A1} is non empty closed Element of bool the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

Cl {X0} is non empty closed Element of bool the carrier of X

A is Element of bool the carrier of X

A /\ (Cl {X0}) is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

A is Element of the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

A is Element of the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

A is set

D is Element of the carrier of X

{D} is non empty trivial V170(X) Element of bool the carrier of X

Cl {D} is non empty closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Int X0 is open Element of bool the carrier of X

X0 /\ (Int X0) is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

bool the carrier of X is non empty set

Cl {X0} is non empty closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{ b

meet { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

D is set

A1 is Element of bool the carrier of X

A1 is set

D is Element of bool (bool the carrier of X)

A2 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{ b

meet { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

D is set

A1 is Element of bool the carrier of X

A1 is set

D is Element of bool (bool the carrier of X)

A2 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

Cl {X0} is non empty closed Element of bool the carrier of X

{ b

meet { b

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

Cl {X0} is non empty closed Element of bool the carrier of X

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A) is Element of bool the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

Cl {X0} is non empty closed Element of bool the carrier of X

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A) is Element of bool the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

(X,X0) \/ (X,A) is non empty Element of bool the carrier of X

D is Element of the carrier of X

(X,D) is non empty Element of bool the carrier of X

(X,D) is non empty Element of bool (bool the carrier of X)

{ b

union (X,D) is Element of bool the carrier of X

{D} is non empty trivial V170(X) Element of bool the carrier of X

Cl {D} is non empty closed Element of bool the carrier of X

(X,D) is non empty Element of bool the carrier of X

(X,D) is non empty Element of bool (bool the carrier of X)

{ b

union (X,D) is Element of bool the carrier of X

{D} is non empty trivial V170(X) Element of bool the carrier of X

Cl {D} is non empty closed Element of bool the carrier of X

{D} is non empty trivial V170(X) Element of bool the carrier of X

Cl {D} is non empty closed Element of bool the carrier of X

{D} is non empty trivial V170(X) Element of bool the carrier of X

Cl {D} is non empty closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

bool the carrier of X is non empty set

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

Cl {X0} is non empty closed Element of bool the carrier of X

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A) is Element of bool the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

Cl {X0} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {X0}) /\ (meet { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

D is set

A1 is Element of bool the carrier of X

D is Element of bool (bool the carrier of X)

meet D is Element of bool the carrier of X

(Cl {X0}) /\ (meet D) is Element of bool the carrier of X

((Cl {X0}) /\ (meet D)) \ (X,X0) is Element of bool the carrier of X

A1 is set

A2 is Element of the carrier of X

(X,A2) is non empty Element of bool the carrier of X

(X,A2) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A2) is Element of bool the carrier of X

{A2} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A2} is non empty closed Element of bool the carrier of X

(Cl {A2}) ` is open Element of bool the carrier of X

the carrier of X \ (Cl {A2}) is set

A1 is non empty Element of bool the carrier of X

A2 is non empty Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

Cl {X0} is non empty closed Element of bool the carrier of X

A is Element of the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

{ b

meet { b

{ b

meet { b

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

A2 is set

A1 is Element of bool the carrier of X

(Cl {A}) ` is open Element of bool the carrier of X

the carrier of X \ (Cl {A}) is set

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A) is Element of bool the carrier of X

(Cl {A}) /\ (meet { b

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

Cl {X0} is non empty closed Element of bool the carrier of X

A is Element of the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A) is Element of bool the carrier of X

{ b

meet { b

(Cl {A}) /\ (meet { b

{ b

meet { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

A1 is set

A2 is Element of bool the carrier of X

A1 is set

R is Element of bool the carrier of X

A1 is Element of bool (bool the carrier of X)

meet A1 is Element of bool the carrier of X

A1 is Element of bool (bool the carrier of X)

meet A1 is Element of bool the carrier of X

(Cl {A}) /\ (meet A1) is Element of bool the carrier of X

A1 is Element of bool (bool the carrier of X)

meet A1 is Element of bool the carrier of X

(Cl {A}) ` is open Element of bool the carrier of X

the carrier of X \ (Cl {A}) is set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

Cl {X0} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {X0}) /\ (meet { b

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A) is Element of bool the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {A}) /\ (meet { b

(Cl {A}) ` is open Element of bool the carrier of X

the carrier of X \ (Cl {A}) is set

(Cl {X0}) ` is open Element of bool the carrier of X

the carrier of X \ (Cl {X0}) is set

(X,X0) /\ (X,A) is Element of bool the carrier of X

A2 is open Element of bool the carrier of X

(X,X0) \ ((Cl {A}) `) is Element of bool the carrier of X

A1 is set

R is Element of the carrier of X

{R} is non empty trivial V170(X) Element of bool the carrier of X

(X,R) is non empty Element of bool the carrier of X

(X,R) is non empty Element of bool (bool the carrier of X)

{ b

union (X,R) is Element of bool the carrier of X

Cl {R} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {R}) /\ (meet { b

(X,A) \ A2 is Element of bool the carrier of X

c

a is Element of the carrier of X

{a} is non empty trivial V170(X) Element of bool the carrier of X

(X,a) is non empty Element of bool the carrier of X

(X,a) is non empty Element of bool (bool the carrier of X)

{ b

union (X,a) is Element of bool the carrier of X

Cl {a} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {a}) /\ (meet { b

A2 is open Element of bool the carrier of X

D is Element of bool the carrier of X

D is Element of bool the carrier of X

D /\ (X,A) is Element of bool the carrier of X

D is Element of bool the carrier of X

D is Element of bool the carrier of X

D /\ (X,X0) is Element of bool the carrier of X

D is Element of bool the carrier of X

A1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty Element of bool the carrier of X

(X,X0) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,X0) is Element of bool the carrier of X

{X0} is non empty trivial V170(X) Element of bool the carrier of X

Cl {X0} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {X0}) /\ (meet { b

A is Element of the carrier of X

(X,A) is non empty Element of bool the carrier of X

(X,A) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A) is Element of bool the carrier of X

{A} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {A}) /\ (meet { b

D is Element of bool the carrier of X

D is Element of bool the carrier of X

D ` is Element of bool the carrier of X

the carrier of X \ D is set

A1 is Element of bool the carrier of X

A1 is Element of bool the carrier of X

D is Element of bool the carrier of X

D is Element of bool the carrier of X

D ` is Element of bool the carrier of X

the carrier of X \ D is set

A1 is Element of bool the carrier of X

A1 is Element of bool the carrier of X

D is Element of bool the carrier of X

D is Element of bool the carrier of X

D /\ (X,A) is Element of bool the carrier of X

D is Element of bool the carrier of X

D is Element of bool the carrier of X

D /\ (X,X0) is Element of bool the carrier of X

D is Element of bool the carrier of X

A1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

{ b

meet { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

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

D is set

A1 is Element of bool the carrier of X

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

D is Element of bool (bool the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

{ b

meet { b

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Int X0 is open Element of bool the carrier of X

(X,(Int X0)) is Element of bool the carrier of X

{ (X,b

union { (X,b

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

{ b

meet { b

bool the carrier of X is non empty Element of bool (bool the carrier of X)

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

D is set

A1 is Element of bool the carrier of X

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

D is Element of bool (bool the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

Cl X0 is closed Element of bool the carrier of X

{ b

meet { b

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

Cl X0 is closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

(X,(Cl X0)) is Element of bool the carrier of X

{ (X,b

union { (X,b

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

Cl (X,X0) is closed Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

Cl X0 is closed Element of bool the carrier of X

A is Element of bool the carrier of X

(X,A) is Element of bool the carrier of X

{ (X,b

union { (X,b

Cl A is closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

A is Element of bool the carrier of X

X0 /\ A is Element of bool the carrier of X

(X,(X0 /\ A)) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,A) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,X0) /\ (X,A) is Element of bool the carrier of X

D is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A1) is Element of bool the carrier of X

{A1} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A1} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {A1}) /\ (meet { b

{ (X,b

A2 is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A1) is Element of bool the carrier of X

{A1} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A1} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {A1}) /\ (meet { b

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A1) is Element of bool the carrier of X

{A1} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A1} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {A1}) /\ (meet { b

{ (X,b

A2 is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A1) is Element of bool the carrier of X

{A1} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A1} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {A1}) /\ (meet { b

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

(X,X0) is Element of bool the carrier of X

{ (X,b

union { (X,b

A is Element of bool the carrier of X

X0 /\ A is Element of bool the carrier of X

(X,(X0 /\ A)) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,A) is Element of bool the carrier of X

{ (X,b

union { (X,b

(X,X0) /\ (X,A) is Element of bool the carrier of X

D is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A1) is Element of bool the carrier of X

{A1} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A1} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {A1}) /\ (meet { b

{ (X,b

A2 is set

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

{ b

union (X,A1) is Element of bool the carrier of X

{A1} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A1} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {A1}) /\ (meet { b

A1 is Element of the carrier of X

(X,A1) is non empty Element of bool the carrier of X

(X,A1) is non empty Element of bool (bool the carrier of X)

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

{ b

union (X,A1) is Element of bool the carrier of X

{A1} is non empty trivial V170(X) Element of bool the carrier of X

Cl {A1} is non empty closed Element of bool the carrier of X

{ b

meet { b

(Cl {A1}) /\ (meet { b

{ (X,b