:: TMAP_1 semantic presentation

K103() is set

bool K103() is non empty set

K185() is non empty strict TopSpace-like TopStruct

the carrier of K185() is non empty set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set

1 is non empty set

union {} is set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

X is non empty set

bool X is non empty set

X1 is non empty Element of bool X

Y is non empty set

[:X1,Y:] is non empty Relation-like set

bool [:X1,Y:] is non empty set

X2 is non empty Element of bool X

[:X2,Y:] is non empty Relation-like set

bool [:X2,Y:] is non empty set

f1 is non empty Relation-like X1 -defined Y -valued Function-like total V21(X1,Y) Element of bool [:X1,Y:]

X1 /\ X2 is Element of bool X

f1 | (X1 /\ X2) is Relation-like X1 -defined X1 /\ X2 -defined X1 -defined Y -valued Function-like Element of bool [:X1,Y:]

f2 is non empty Relation-like X2 -defined Y -valued Function-like total V21(X2,Y) Element of bool [:X2,Y:]

f2 | (X1 /\ X2) is Relation-like X2 -defined X1 /\ X2 -defined X2 -defined Y -valued Function-like Element of bool [:X2,Y:]

X1 \/ X2 is non empty Element of bool X

[:(X1 \/ X2),Y:] is non empty Relation-like set

bool [:(X1 \/ X2),Y:] is non empty set

f2 +* f1 is Relation-like Function-like set

f1 +* f2 is Relation-like Function-like set

rng (f1 +* f2) is set

rng f1 is non empty Element of bool Y

bool Y is non empty set

rng f2 is non empty Element of bool Y

(rng f1) \/ (rng f2) is non empty Element of bool Y

rng (f2 +* f1) is set

(rng f2) \/ (rng f1) is non empty Element of bool Y

dom f1 is non empty Element of bool X1

bool X1 is non empty set

dom f2 is non empty Element of bool X2

bool X2 is non empty set

dom (f1 +* f2) is set

dom (f2 +* f1) is set

f is non empty Relation-like X1 \/ X2 -defined Y -valued Function-like total V21(X1 \/ X2,Y) Element of bool [:(X1 \/ X2),Y:]

f | X1 is Relation-like X1 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

f | X2 is Relation-like X2 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

g is non empty Element of bool X

a is Element of g

(f1 +* f2) . a is set

f2 . a is set

X1 \ X2 is Element of bool X

f1 . a is set

a is Element of g

(f2 +* f1) . a is set

f1 . a is set

X2 \ X1 is Element of bool X

f2 . a is set

a is Element of g

f . a is set

f2 . a is set

f1 . a is set

(f2 | (X1 /\ X2)) . a is set

v is non empty Relation-like X1 \/ X2 -defined Y -valued Function-like total V21(X1 \/ X2,Y) Element of bool [:(X1 \/ X2),Y:]

v . a is set

X1 \+\ X2 is Element of bool X

X1 \ X2 is set

X2 \ X1 is set

(X1 \ X2) \/ (X2 \ X1) is set

(X1 \+\ X2) \/ (X1 /\ X2) is Element of bool X

bool g is non empty set

a is Element of g

f . a is set

v . a is set

f1 . a is set

f3 is non empty Relation-like X1 \/ X2 -defined Y -valued Function-like total V21(X1 \/ X2,Y) Element of bool [:(X1 \/ X2),Y:]

f3 | X1 is Relation-like X1 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

f3 | X2 is Relation-like X2 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

g is non empty Relation-like X1 \/ X2 -defined Y -valued Function-like total V21(X1 \/ X2,Y) Element of bool [:(X1 \/ X2),Y:]

g | X1 is Relation-like X1 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

g | X2 is Relation-like X2 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

g is non empty Element of bool X

f is Element of g

f3 . f is set

(g | X2) . f is set

g . f is set

(g | X1) . f is set

X is non empty set

bool X is non empty set

Y is non empty set

X1 is non empty Element of bool X

X2 is non empty Element of bool X

[:X1,Y:] is non empty Relation-like set

bool [:X1,Y:] is non empty set

[:X2,Y:] is non empty Relation-like set

bool [:X2,Y:] is non empty set

X1 /\ X2 is Element of bool X

X1 \/ X2 is non empty Element of bool X

f1 is non empty Relation-like X1 -defined Y -valued Function-like total V21(X1,Y) Element of bool [:X1,Y:]

f1 | (X1 /\ X2) is Relation-like X1 -defined X1 /\ X2 -defined X1 -defined Y -valued Function-like Element of bool [:X1,Y:]

f2 is non empty Relation-like X2 -defined Y -valued Function-like total V21(X2,Y) Element of bool [:X2,Y:]

f2 | (X1 /\ X2) is Relation-like X2 -defined X1 /\ X2 -defined X2 -defined Y -valued Function-like Element of bool [:X2,Y:]

(X,Y,X1,X2,f1,f2) is non empty Relation-like X1 \/ X2 -defined Y -valued Function-like total V21(X1 \/ X2,Y) Element of bool [:(X1 \/ X2),Y:]

[:(X1 \/ X2),Y:] is non empty Relation-like set

bool [:(X1 \/ X2),Y:] is non empty set

(X,Y,X1,X2,f1,f2) | X1 is Relation-like X1 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

(X,Y,X1,X2,f1,f2) | X2 is Relation-like X2 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

[:{},Y:] is Relation-like set

bool [:{},Y:] is non empty set

f3 is empty Relation-like non-empty empty-yielding {} -defined Y -valued Function-like one-to-one constant functional total V21( {} ,Y) Element of bool [:{},Y:]

g is empty Relation-like non-empty empty-yielding {} -defined Y -valued Function-like one-to-one constant functional total V21( {} ,Y) Element of bool [:{},Y:]

X is non empty set

bool X is non empty set

Y is non empty set

X1 is non empty Element of bool X

[:X1,Y:] is non empty Relation-like set

bool [:X1,Y:] is non empty set

X2 is non empty Element of bool X

X1 \/ X2 is non empty Element of bool X

[:(X1 \/ X2),Y:] is non empty Relation-like set

bool [:(X1 \/ X2),Y:] is non empty set

[:X2,Y:] is non empty Relation-like set

bool [:X2,Y:] is non empty set

f1 is non empty Relation-like X1 \/ X2 -defined Y -valued Function-like total V21(X1 \/ X2,Y) Element of bool [:(X1 \/ X2),Y:]

f1 | X1 is Relation-like X1 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

f1 | X2 is Relation-like X2 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

f2 is non empty Relation-like X1 -defined Y -valued Function-like total V21(X1,Y) Element of bool [:X1,Y:]

g is non empty Relation-like X2 -defined Y -valued Function-like total V21(X2,Y) Element of bool [:X2,Y:]

(X,Y,X1,X2,f2,g) is non empty Relation-like X1 \/ X2 -defined Y -valued Function-like total V21(X1 \/ X2,Y) Element of bool [:(X1 \/ X2),Y:]

X1 /\ X2 is Element of bool X

g is non empty Relation-like X1 -defined Y -valued Function-like total V21(X1,Y) Element of bool [:X1,Y:]

g | (X1 /\ X2) is Relation-like X1 -defined X1 /\ X2 -defined X1 -defined Y -valued Function-like Element of bool [:X1,Y:]

f1 | (X1 /\ X2) is Relation-like X1 \/ X2 -defined X1 /\ X2 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

f3 is non empty Relation-like X2 -defined Y -valued Function-like total V21(X2,Y) Element of bool [:X2,Y:]

f3 | (X1 /\ X2) is Relation-like X2 -defined X1 /\ X2 -defined X2 -defined Y -valued Function-like Element of bool [:X2,Y:]

X is non empty set

bool X is non empty set

Y is non empty set

X1 is non empty Element of bool X

[:X1,Y:] is non empty Relation-like set

bool [:X1,Y:] is non empty set

X2 is non empty Element of bool X

[:X2,Y:] is non empty Relation-like set

bool [:X2,Y:] is non empty set

X1 /\ X2 is Element of bool X

X1 \/ X2 is non empty Element of bool X

X2 \/ X1 is non empty Element of bool X

f1 is non empty Relation-like X1 -defined Y -valued Function-like total V21(X1,Y) Element of bool [:X1,Y:]

f1 | (X1 /\ X2) is Relation-like X1 -defined X1 /\ X2 -defined X1 -defined Y -valued Function-like Element of bool [:X1,Y:]

f2 is non empty Relation-like X2 -defined Y -valued Function-like total V21(X2,Y) Element of bool [:X2,Y:]

f2 | (X1 /\ X2) is Relation-like X2 -defined X1 /\ X2 -defined X2 -defined Y -valued Function-like Element of bool [:X2,Y:]

(X,Y,X1,X2,f1,f2) is non empty Relation-like X1 \/ X2 -defined Y -valued Function-like total V21(X1 \/ X2,Y) Element of bool [:(X1 \/ X2),Y:]

[:(X1 \/ X2),Y:] is non empty Relation-like set

bool [:(X1 \/ X2),Y:] is non empty set

(X,Y,X2,X1,f2,f1) is non empty Relation-like X2 \/ X1 -defined Y -valued Function-like total V21(X2 \/ X1,Y) Element of bool [:(X2 \/ X1),Y:]

[:(X2 \/ X1),Y:] is non empty Relation-like set

bool [:(X2 \/ X1),Y:] is non empty set

(X,Y,X1,X2,f1,f2) | X1 is Relation-like X1 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

(X,Y,X1,X2,f1,f2) | X2 is Relation-like X2 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

X is non empty set

bool X is non empty set

Y is non empty set

X1 is non empty Element of bool X

[:X1,Y:] is non empty Relation-like set

bool [:X1,Y:] is non empty set

X2 is non empty Element of bool X

X1 \/ X2 is non empty Element of bool X

[:X2,Y:] is non empty Relation-like set

bool [:X2,Y:] is non empty set

X1 /\ X2 is Element of bool X

f1 is non empty Element of bool X

X2 \/ f1 is non empty Element of bool X

[:f1,Y:] is non empty Relation-like set

bool [:f1,Y:] is non empty set

X2 /\ f1 is Element of bool X

X1 /\ f1 is Element of bool X

f2 is non empty Element of bool X

g is non empty Element of bool X

[:f2,Y:] is non empty Relation-like set

bool [:f2,Y:] is non empty set

[:g,Y:] is non empty Relation-like set

bool [:g,Y:] is non empty set

f2 \/ f1 is non empty Element of bool X

X1 \/ g is non empty Element of bool X

f3 is non empty Relation-like X1 -defined Y -valued Function-like total V21(X1,Y) Element of bool [:X1,Y:]

f3 | (X1 /\ X2) is Relation-like X1 -defined X1 /\ X2 -defined X1 -defined Y -valued Function-like Element of bool [:X1,Y:]

f3 | (X1 /\ f1) is Relation-like X1 -defined X1 /\ f1 -defined X1 -defined Y -valued Function-like Element of bool [:X1,Y:]

g is non empty Relation-like X2 -defined Y -valued Function-like total V21(X2,Y) Element of bool [:X2,Y:]

g | (X1 /\ X2) is Relation-like X2 -defined X1 /\ X2 -defined X2 -defined Y -valued Function-like Element of bool [:X2,Y:]

g | (X2 /\ f1) is Relation-like X2 -defined X2 /\ f1 -defined X2 -defined Y -valued Function-like Element of bool [:X2,Y:]

(X,Y,X1,X2,f3,g) is non empty Relation-like X1 \/ X2 -defined Y -valued Function-like total V21(X1 \/ X2,Y) Element of bool [:(X1 \/ X2),Y:]

[:(X1 \/ X2),Y:] is non empty Relation-like set

bool [:(X1 \/ X2),Y:] is non empty set

f is non empty Relation-like f1 -defined Y -valued Function-like total V21(f1,Y) Element of bool [:f1,Y:]

f | (X2 /\ f1) is Relation-like f1 -defined X2 /\ f1 -defined f1 -defined Y -valued Function-like Element of bool [:f1,Y:]

f | (X1 /\ f1) is Relation-like f1 -defined X1 /\ f1 -defined f1 -defined Y -valued Function-like Element of bool [:f1,Y:]

(X,Y,X2,f1,g,f) is non empty Relation-like X2 \/ f1 -defined Y -valued Function-like total V21(X2 \/ f1,Y) Element of bool [:(X2 \/ f1),Y:]

[:(X2 \/ f1),Y:] is non empty Relation-like set

bool [:(X2 \/ f1),Y:] is non empty set

v is non empty Relation-like f2 -defined Y -valued Function-like total V21(f2,Y) Element of bool [:f2,Y:]

(X,Y,f2,f1,v,f) is non empty Relation-like f2 \/ f1 -defined Y -valued Function-like total V21(f2 \/ f1,Y) Element of bool [:(f2 \/ f1),Y:]

[:(f2 \/ f1),Y:] is non empty Relation-like set

bool [:(f2 \/ f1),Y:] is non empty set

a is non empty Relation-like g -defined Y -valued Function-like total V21(g,Y) Element of bool [:g,Y:]

(X,Y,X1,g,f3,a) is non empty Relation-like X1 \/ g -defined Y -valued Function-like total V21(X1 \/ g,Y) Element of bool [:(X1 \/ g),Y:]

[:(X1 \/ g),Y:] is non empty Relation-like set

bool [:(X1 \/ g),Y:] is non empty set

v | X2 is Relation-like X2 -defined f2 -defined Y -valued Function-like Element of bool [:f2,Y:]

(v | X2) | (X2 /\ f1) is Relation-like X2 /\ f1 -defined X2 -defined f2 -defined Y -valued Function-like Element of bool [:f2,Y:]

f2 /\ f1 is Element of bool X

[:(f2 /\ f1),Y:] is Relation-like set

bool [:(f2 /\ f1),Y:] is non empty set

v | (f2 /\ f1) is Relation-like f2 -defined f2 /\ f1 -defined f2 -defined Y -valued Function-like Element of bool [:f2,Y:]

g1 is non empty Relation-like X1 \/ g -defined Y -valued Function-like total V21(X1 \/ g,Y) Element of bool [:(X1 \/ g),Y:]

g1 | g is Relation-like g -defined X1 \/ g -defined Y -valued Function-like Element of bool [:(X1 \/ g),Y:]

f | (f2 /\ f1) is Relation-like f1 -defined f2 /\ f1 -defined f1 -defined Y -valued Function-like Element of bool [:f1,Y:]

v | X1 is Relation-like X1 -defined f2 -defined Y -valued Function-like Element of bool [:f2,Y:]

(v | X1) | (X1 /\ f1) is Relation-like X1 /\ f1 -defined X1 -defined f2 -defined Y -valued Function-like Element of bool [:f2,Y:]

c

g2 is Relation-like f2 /\ f1 -defined Y -valued Function-like total V21(f2 /\ f1,Y) Element of bool [:(f2 /\ f1),Y:]

g2 . c

g2 | (X1 /\ f1) is Relation-like X1 /\ f1 -defined f2 /\ f1 -defined Y -valued Function-like Element of bool [:(f2 /\ f1),Y:]

(g2 | (X1 /\ f1)) . c

v | (X1 /\ f1) is Relation-like X1 /\ f1 -defined f2 -defined Y -valued Function-like Element of bool [:f2,Y:]

(v | (X1 /\ f1)) . c

(f | (X1 /\ f1)) . c

F is Relation-like f2 /\ f1 -defined Y -valued Function-like total V21(f2 /\ f1,Y) Element of bool [:(f2 /\ f1),Y:]

F | (X1 /\ f1) is Relation-like X1 /\ f1 -defined f2 /\ f1 -defined Y -valued Function-like Element of bool [:(f2 /\ f1),Y:]

(F | (X1 /\ f1)) . c

F . c

g2 | (X2 /\ f1) is Relation-like X2 /\ f1 -defined f2 /\ f1 -defined Y -valued Function-like Element of bool [:(f2 /\ f1),Y:]

(g2 | (X2 /\ f1)) . c

v | (X2 /\ f1) is Relation-like X2 /\ f1 -defined f2 -defined Y -valued Function-like Element of bool [:f2,Y:]

(v | (X2 /\ f1)) . c

(f | (X2 /\ f1)) . c

F | (X2 /\ f1) is Relation-like X2 /\ f1 -defined f2 /\ f1 -defined Y -valued Function-like Element of bool [:(f2 /\ f1),Y:]

(F | (X2 /\ f1)) . c

(X1 /\ f1) \/ (X2 /\ f1) is Element of bool X

g1 | f2 is Relation-like f2 -defined X1 \/ g -defined Y -valued Function-like Element of bool [:(X1 \/ g),Y:]

(g1 | f2) | X1 is Relation-like X1 -defined f2 -defined X1 \/ g -defined Y -valued Function-like Element of bool [:(X1 \/ g),Y:]

(g1 | f2) | X2 is Relation-like X2 -defined f2 -defined X1 \/ g -defined Y -valued Function-like Element of bool [:(X1 \/ g),Y:]

g1 | X2 is Relation-like X2 -defined X1 \/ g -defined Y -valued Function-like Element of bool [:(X1 \/ g),Y:]

c

G is non empty Relation-like g -defined Y -valued Function-like total V21(g,Y) Element of bool [:g,Y:]

G . c

g1 . c

g . c

a | X2 is Relation-like X2 -defined g -defined Y -valued Function-like Element of bool [:g,Y:]

(a | X2) . c

a . c

g1 | f1 is Relation-like f1 -defined X1 \/ g -defined Y -valued Function-like Element of bool [:(X1 \/ g),Y:]

(g1 | f1) . c

f . c

a | f1 is Relation-like f1 -defined g -defined Y -valued Function-like Element of bool [:g,Y:]

(a | f1) . c

g1 | X1 is Relation-like X1 -defined X1 \/ g -defined Y -valued Function-like Element of bool [:(X1 \/ g),Y:]

X is non empty set

bool X is non empty set

Y is non empty set

X1 is non empty Element of bool X

[:X1,Y:] is non empty Relation-like set

bool [:X1,Y:] is non empty set

bool X1 is non empty set

X2 is non empty Element of bool X

[:X2,Y:] is non empty Relation-like set

bool [:X2,Y:] is non empty set

X1 /\ X2 is Element of bool X

bool X2 is non empty set

X1 \/ X2 is non empty Element of bool X

f1 is non empty Relation-like X1 -defined Y -valued Function-like total V21(X1,Y) Element of bool [:X1,Y:]

f1 | (X1 /\ X2) is Relation-like X1 -defined X1 /\ X2 -defined X1 -defined Y -valued Function-like Element of bool [:X1,Y:]

f2 is non empty Relation-like X2 -defined Y -valued Function-like total V21(X2,Y) Element of bool [:X2,Y:]

f2 | (X1 /\ X2) is Relation-like X2 -defined X1 /\ X2 -defined X2 -defined Y -valued Function-like Element of bool [:X2,Y:]

(X,Y,X1,X2,f1,f2) is non empty Relation-like X1 \/ X2 -defined Y -valued Function-like total V21(X1 \/ X2,Y) Element of bool [:(X1 \/ X2),Y:]

[:(X1 \/ X2),Y:] is non empty Relation-like set

bool [:(X1 \/ X2),Y:] is non empty set

(X,Y,X1,X2,f1,f2) | (X1 \/ X2) is Relation-like X1 \/ X2 -defined X1 \/ X2 -defined Y -valued Function-like Element of bool [:(X1 \/ X2),Y:]

id (X1 \/ X2) is non empty Relation-like X1 \/ X2 -defined X1 \/ X2 -valued Function-like one-to-one total V21(X1 \/ X2,X1 \/ X2) V22(X1 \/ X2) V23(X1 \/ X2,X1 \/ X2) V69() V71() V72() V76() Element of bool [:(X1 \/ X2),(X1 \/ X2):]

[:(X1 \/ X2),(X1 \/ X2):] is non empty Relation-like set

bool [:(X1 \/ X2),(X1 \/ X2):] is non empty set

(X,Y,X1,X2,f1,f2) * (id (X1 \/ X2)) is non empty Relation-like X1 \/ X2 -defined Y -valued Function-like total V21(X1 \/ X2,Y) Element of bool [:(X1 \/ X2),Y:]

dom (X,Y,X1,X2,f1,f2) is non empty Element of bool (X1 \/ X2)

bool (X1 \/ X2) is non empty set

dom f2 is non empty Element of bool X2

dom f1 is non empty Element of bool X1

X is TopStruct

Y is SubSpace of X

the carrier of Y is set

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

bool the carrier of Y is non empty set

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

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

X1 is TopStruct

[#] Y is non proper Element of bool the carrier of Y

[#] X1 is non proper Element of bool the carrier of X1

the carrier of X1 is set

bool the carrier of X1 is non empty set

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

the carrier of X is set

bool the carrier of X is non empty set

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

bool (bool the carrier of X1) 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

X2 is Element of bool the carrier of X1

f1 is Element of bool the carrier of X

f1 /\ ([#] X1) is Element of bool the carrier of X1

X is TopStruct

Y is TopSpace-like TopStruct

X1 is TopSpace-like TopStruct

the carrier of X1 is set

the topology of X1 is non empty Element of bool (bool the carrier of X1)

bool the carrier of X1 is non empty set

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

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

[#] Y is non proper open closed Element of bool the carrier of Y

the carrier of Y is set

bool the carrier of Y is non empty set

[#] X1 is non proper open closed Element of bool the carrier of X1

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

the carrier of X is set

bool the carrier of X 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

X2 is Element of bool the carrier of X1

f1 is Element of bool the carrier of X

f1 /\ ([#] X1) is Element of bool the carrier of X1

X is TopSpace-like TopStruct

X1 is TopSpace-like TopStruct

Y is TopSpace-like TopStruct

the carrier of Y is set

the topology of Y is non empty Element of bool (bool the carrier of Y)

bool the carrier of Y is non empty set

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

TopStruct(# the carrier of Y, the topology of Y #) is strict TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X2 is TopSpace-like SubSpace of X

the carrier of X2 is set

f1 is Element of bool the carrier of X

the carrier of X is set

bool the carrier of X is non empty set

X2 is TopSpace-like SubSpace of X

the carrier of X2 is set

f1 is Element of bool the carrier of X

X is TopSpace-like TopStruct

X1 is TopSpace-like TopStruct

Y is TopSpace-like TopStruct

the carrier of Y is set

the topology of Y is non empty Element of bool (bool the carrier of Y)

bool the carrier of Y is non empty set

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

TopStruct(# the carrier of Y, the topology of Y #) is strict TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X2 is TopSpace-like SubSpace of X

the carrier of X2 is set

f1 is Element of bool the carrier of X

the carrier of X is set

bool the carrier of X is non empty set

X2 is TopSpace-like SubSpace of X

the carrier of X2 is set

f1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

the carrier of Y is non empty set

X1 is non empty TopSpace-like SubSpace of X

the carrier of X1 is non empty set

X2 is Element of the carrier of Y

f1 is Element of the carrier of X1

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

the carrier of Y is non empty set

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

the carrier of (Y union X1) is non empty set

the carrier of X1 is non empty set

X2 is Element of the carrier of (Y union X1)

the carrier of X is non empty set

bool the carrier of X is non empty set

f1 is Element of bool the carrier of X

f2 is Element of bool the carrier of X

g is Element of bool the carrier of X

f2 \/ g is Element of bool the carrier of X

f3 is Element of the carrier of X1

f3 is Element of the carrier of X1

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

the carrier of Y is non empty set

X1 is non empty TopSpace-like SubSpace of X

Y meet X1 is non empty strict TopSpace-like SubSpace of X

the carrier of (Y meet X1) is non empty set

the carrier of X1 is non empty set

the carrier of X is non empty set

bool the carrier of X is non empty set

g is Element of the carrier of (Y meet X1)

f2 is Element of bool the carrier of X

f1 is Element of bool the carrier of X

X2 is Element of bool the carrier of X

f1 /\ X2 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

the carrier of Y is non empty set

bool the carrier of Y is non empty set

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

the carrier of (Y union X1) is non empty set

the carrier of X1 is non empty set

bool the carrier of X1 is non empty set

bool the carrier of (Y union X1) is non empty set

X2 is Element of the carrier of (Y union X1)

f1 is Element of bool the carrier of Y

f2 is Element of bool the carrier of X1

f1 \/ f2 is set

[#] Y is non empty non proper open closed Element of bool the carrier of Y

f3 is Element of bool the carrier of (Y union X1)

f3 /\ ([#] Y) is Element of bool the carrier of Y

[#] X1 is non empty non proper open closed Element of bool the carrier of X1

f is Element of bool the carrier of (Y union X1)

f /\ ([#] X1) is Element of bool the carrier of X1

f3 /\ f is Element of bool the carrier of (Y union X1)

v is Element of bool the carrier of (Y union X1)

g is Element of bool the carrier of (Y union X1)

v /\ g is Element of bool the carrier of (Y union X1)

f3 /\ g is Element of bool the carrier of (Y union X1)

g is Element of bool the carrier of (Y union X1)

v /\ g is Element of bool the carrier of (Y union X1)

f /\ g is Element of bool the carrier of (Y union X1)

g \/ g is Element of bool the carrier of (Y union X1)

v /\ (g \/ g) is Element of bool the carrier of (Y union X1)

(v /\ g) \/ (v /\ g) is Element of bool the carrier of (Y union X1)

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

the carrier of Y is non empty set

bool the carrier of Y is non empty set

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

the carrier of (Y union X1) is non empty set

the carrier of X1 is non empty set

bool the carrier of X1 is non empty set

bool the carrier of (Y union X1) is non empty set

X2 is Element of the carrier of (Y union X1)

f1 is Element of bool the carrier of Y

f2 is Element of bool the carrier of X1

f1 \/ f2 is set

[#] Y is non empty non proper open closed Element of bool the carrier of Y

f3 is Element of bool the carrier of (Y union X1)

f3 /\ ([#] Y) is Element of bool the carrier of Y

[#] X1 is non empty non proper open closed Element of bool the carrier of X1

f is Element of bool the carrier of (Y union X1)

f /\ ([#] X1) is Element of bool the carrier of X1

f3 /\ f is Element of bool the carrier of (Y union X1)

v is Element of bool the carrier of (Y union X1)

g is Element of bool the carrier of (Y union X1)

v /\ g is Element of bool the carrier of (Y union X1)

f3 /\ g is Element of bool the carrier of (Y union X1)

g is Element of bool the carrier of (Y union X1)

v /\ g is Element of bool the carrier of (Y union X1)

f /\ g is Element of bool the carrier of (Y union X1)

g \/ g is Element of bool the carrier of (Y union X1)

v /\ (g \/ g) is Element of bool the carrier of (Y union X1)

(v /\ g) \/ (v /\ g) is Element of bool the carrier of (Y union X1)

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

the carrier of Y is non empty set

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

the carrier of (Y union X1) is non empty set

the carrier of X1 is non empty set

bool the carrier of (Y union X1) is non empty set

X2 is Element of the carrier of (Y union X1)

f1 is Element of the carrier of Y

f2 is Element of the carrier of X1

g is a_neighborhood of f1

f3 is a_neighborhood of f2

g \/ f3 is set

bool the carrier of Y is non empty set

g is Element of bool the carrier of Y

bool the carrier of X1 is non empty set

f is Element of bool the carrier of X1

g \/ f is set

v is Element of bool the carrier of (Y union X1)

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

the carrier of Y is non empty set

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

the carrier of (Y union X1) is non empty set

the carrier of X1 is non empty set

X2 is Element of the carrier of (Y union X1)

f1 is Element of the carrier of Y

f2 is Element of the carrier of X1

g is a_neighborhood of f1

f3 is a_neighborhood of f2

g \/ f3 is set

bool the carrier of (Y union X1) is non empty set

g is Element of bool the carrier of (Y union X1)

f is a_neighborhood of X2

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

the carrier of Y is non empty set

the carrier of X1 is non empty set

the carrier of Y /\ the carrier of X1 is set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of Y is non empty set

the carrier of X1 is non empty set

the carrier of X2 is non empty set

f1 is Element of bool the carrier of X

f2 is Element of bool the carrier of X

g is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of Y is non empty set

the carrier of X1 is non empty set

the carrier of X2 is non empty set

f1 is Element of bool the carrier of X

f2 is Element of bool the carrier of X

g is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

Y union Y is non empty strict TopSpace-like SubSpace of X

the carrier of Y is non empty set

the topology of Y is non empty Element of bool (bool the carrier of Y)

bool the carrier of Y is non empty set

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

TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

Y meet Y is non empty strict TopSpace-like SubSpace of X

the carrier of Y is non empty set

the topology of Y is non empty Element of bool (bool the carrier of Y)

bool the carrier of Y is non empty set

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

TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

Y union X2 is non empty strict TopSpace-like SubSpace of X

f1 is non empty TopSpace-like SubSpace of X

X1 union f1 is non empty strict TopSpace-like SubSpace of X

the carrier of Y is non empty set

the carrier of X1 is non empty set

the carrier of X2 is non empty set

the carrier of f1 is non empty set

the carrier of Y \/ the carrier of X2 is non empty set

the carrier of X1 \/ the carrier of f1 is non empty set

the carrier of (Y union X2) is non empty set

the carrier of (X1 union f1) is non empty set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y meet X1 is non empty strict TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

f1 is non empty TopSpace-like SubSpace of X

X2 meet f1 is non empty strict TopSpace-like SubSpace of X

the carrier of Y is non empty set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

the carrier of f1 is non empty set

the carrier of Y /\ the carrier of X1 is set

the carrier of X2 /\ the carrier of f1 is set

the carrier of (X2 meet f1) is non empty set

the carrier of (Y meet X1) is non empty set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

Y union X2 is non empty strict TopSpace-like SubSpace of X

the carrier of Y is non empty set

the carrier of X1 is non empty set

the carrier of X2 is non empty set

the carrier of Y \/ the carrier of X2 is non empty set

the carrier of (Y union X2) is non empty set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y meet X1 is non empty strict TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

the carrier of Y is non empty set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

the carrier of Y \/ the carrier of X1 is non empty set

the carrier of Y /\ the carrier of X1 is set

the carrier of (Y meet X1) is non empty set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y meet X1 is non empty strict TopSpace-like SubSpace of X

X1 meet Y is non empty strict TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

Y union X2 is non empty strict TopSpace-like SubSpace of X

(Y union X2) meet X1 is non empty strict TopSpace-like SubSpace of X

X2 meet X1 is non empty strict TopSpace-like SubSpace of X

X1 meet (Y union X2) is non empty strict TopSpace-like SubSpace of X

X1 meet X2 is non empty strict TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X1 is non empty set

the carrier of Y is non empty set

the carrier of X2 is non empty set

f2 is Element of bool the carrier of X

f1 is Element of bool the carrier of X

the carrier of (X1 meet (Y union X2)) is non empty set

the carrier of (Y union X2) is non empty set

f1 /\ the carrier of (Y union X2) is Element of bool the carrier of X

g is Element of bool the carrier of X

f2 \/ g is Element of bool the carrier of X

f1 /\ (f2 \/ g) is Element of bool the carrier of X

f1 /\ f2 is Element of bool the carrier of X

f1 /\ g is Element of bool the carrier of X

(f1 /\ f2) \/ (f1 /\ g) is Element of bool the carrier of X

{} \/ (f1 /\ g) is set

the carrier of (X1 meet X2) is non empty set

the carrier of ((Y union X2) meet X1) is non empty set

the carrier of (Y union X2) /\ f1 is Element of bool the carrier of X

(f2 \/ g) /\ f1 is Element of bool the carrier of X

f2 /\ f1 is Element of bool the carrier of X

g /\ f1 is Element of bool the carrier of X

(f2 /\ f1) \/ (g /\ f1) is Element of bool the carrier of X

{} \/ (g /\ f1) is set

the carrier of (X2 meet X1) is non empty set

g is Element of bool the carrier of X

f1 is Element of bool the carrier of X

the carrier of (X1 meet (Y union X2)) is non empty set

the carrier of (Y union X2) is non empty set

f1 /\ the carrier of (Y union X2) is Element of bool the carrier of X

f2 is Element of bool the carrier of X

f2 \/ g is Element of bool the carrier of X

f1 /\ (f2 \/ g) is Element of bool the carrier of X

f1 /\ f2 is Element of bool the carrier of X

f1 /\ g is Element of bool the carrier of X

(f1 /\ f2) \/ (f1 /\ g) is Element of bool the carrier of X

(f1 /\ f2) \/ {} is set

the carrier of (X1 meet Y) is non empty set

the carrier of ((Y union X2) meet X1) is non empty set

the carrier of (Y union X2) /\ f1 is Element of bool the carrier of X

(f2 \/ g) /\ f1 is Element of bool the carrier of X

f2 /\ f1 is Element of bool the carrier of X

g /\ f1 is Element of bool the carrier of X

(f2 /\ f1) \/ (g /\ f1) is Element of bool the carrier of X

(f2 /\ f1) \/ {} is set

the carrier of (Y meet X1) is non empty set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y meet X1 is non empty strict TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

X2 meet X1 is non empty strict TopSpace-like SubSpace of X

Y meet X2 is non empty strict TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X2 is non empty set

the carrier of Y is non empty set

the carrier of X1 is non empty set

the carrier of (Y meet X1) is non empty set

f2 is Element of bool the carrier of X

g is Element of bool the carrier of X

f2 /\ g is Element of bool the carrier of X

f1 is Element of bool the carrier of X

f2 /\ f1 is Element of bool the carrier of X

the carrier of (Y meet X2) is non empty set

f1 /\ g is Element of bool the carrier of X

the carrier of (X2 meet X1) is non empty set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

the carrier of Y is non empty set

the topology of Y is non empty Element of bool (bool the carrier of Y)

bool the carrier of Y is non empty set

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

TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

Y union X2 is non empty strict TopSpace-like SubSpace of X

X1 meet (Y union X2) is non empty strict TopSpace-like SubSpace of X

X2 union Y is non empty strict TopSpace-like SubSpace of X

X1 meet (X2 union Y) is non empty strict TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X1 is non empty set

the carrier of X2 is non empty set

f2 is Element of bool the carrier of X

f1 is Element of bool the carrier of X

g is Element of bool the carrier of X

the carrier of (X1 meet (Y union X2)) is non empty set

the carrier of (Y union X2) is non empty set

f1 /\ the carrier of (Y union X2) is Element of bool the carrier of X

f2 \/ g is Element of bool the carrier of X

f1 /\ (f2 \/ g) is Element of bool the carrier of X

f1 /\ f2 is Element of bool the carrier of X

f1 /\ g is Element of bool the carrier of X

(f1 /\ f2) \/ (f1 /\ g) is Element of bool the carrier of X

(f1 /\ f2) \/ {} is set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

X2 meet X1 is non empty strict TopSpace-like SubSpace of X

X1 meet X2 is non empty strict TopSpace-like SubSpace of X

Y meet X2 is non empty strict TopSpace-like SubSpace of X

X2 meet Y is non empty strict TopSpace-like SubSpace of X

Y meet X1 is non empty strict TopSpace-like SubSpace of X

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

Y union X2 is non empty strict TopSpace-like SubSpace of X

f1 is non empty TopSpace-like SubSpace of X

X1 meet f1 is non empty strict TopSpace-like SubSpace of X

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

X2 meet (Y union X1) is non empty strict TopSpace-like SubSpace of X

f1 is non empty TopSpace-like SubSpace of X

X2 union f1 is non empty strict TopSpace-like SubSpace of X

f1 meet (Y union X1) is non empty strict TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of Y is non empty set

the carrier of X1 is non empty set

the carrier of X2 is non empty set

the carrier of f1 is non empty set

the carrier of (Y union X1) is non empty set

f2 is Element of bool the carrier of X

g is Element of bool the carrier of X

f2 \/ g is Element of bool the carrier of X

the carrier of (X2 union f1) is non empty set

f3 is Element of bool the carrier of X

g is Element of bool the carrier of X

f3 \/ g is Element of bool the carrier of X

(f3 \/ g) /\ (f2 \/ g) is Element of bool the carrier of X

f3 /\ (f2 \/ g) is Element of bool the carrier of X

g /\ (f2 \/ g) is Element of bool the carrier of X

(f3 /\ (f2 \/ g)) \/ (g /\ (f2 \/ g)) is Element of bool the carrier of X

(f3 /\ (f2 \/ g)) \/ {} is set

the carrier of (X2 meet (Y union X1)) is non empty set

{} \/ (g /\ (f2 \/ g)) is set

the carrier of (f1 meet (Y union X1)) is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

the topology of X 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

TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

Y meet X1 is non empty strict TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

X2 meet (Y union X1) is non empty strict TopSpace-like SubSpace of X

f1 is non empty TopSpace-like SubSpace of X

X2 union f1 is non empty strict TopSpace-like SubSpace of X

f1 meet (Y union X1) is non empty strict TopSpace-like SubSpace of X

f2 is non empty TopSpace-like SubSpace of X

(X2 union f1) union f2 is non empty strict TopSpace-like SubSpace of X

f2 meet (Y union X1) is non empty strict TopSpace-like SubSpace of X

the carrier of f2 is non empty set

the carrier of f1 is non empty set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

the carrier of Y is non empty set

the carrier of (Y union X1) is non empty set

v is Element of bool the carrier of X

f is Element of bool the carrier of X

v \/ f is Element of bool the carrier of X

the carrier of (X2 union f1) is non empty set

g is Element of bool the carrier of X

f3 is Element of bool the carrier of X

g \/ f3 is Element of bool the carrier of X

g is Element of bool the carrier of X

(g \/ f3) \/ g is Element of bool the carrier of X

f3 \/ g is Element of bool the carrier of X

(f3 \/ g) \/ g is Element of bool the carrier of X

((f3 \/ g) \/ g) /\ (v \/ f) is Element of bool the carrier of X

g \/ g is Element of bool the carrier of X

f3 \/ (g \/ g) is Element of bool the carrier of X

(f3 \/ (g \/ g)) /\ (v \/ f) is Element of bool the carrier of X

f3 /\ (v \/ f) is Element of bool the carrier of X

(g \/ g) /\ (v \/ f) is Element of bool the carrier of X

(f3 /\ (v \/ f)) \/ ((g \/ g) /\ (v \/ f)) is Element of bool the carrier of X

{} \/ ((g \/ g) /\ (v \/ f)) is set

g /\ (v \/ f) is Element of bool the carrier of X

g /\ (v \/ f) is Element of bool the carrier of X

(g /\ (v \/ f)) \/ (g /\ (v \/ f)) is Element of bool the carrier of X

the carrier of (X2 meet (Y union X1)) is non empty set

the carrier of (f2 meet (Y union X1)) is non empty set

the carrier of (Y meet X1) is non empty set

v /\ f is Element of bool the carrier of X

v \/ (v /\ f) is Element of bool the carrier of X

the carrier of (f2 meet (Y union X1)) is non empty set

the carrier of (Y meet X1) is non empty set

v /\ f is Element of bool the carrier of X

((g \/ f3) \/ g) /\ (v \/ f) is Element of bool the carrier of X

f3 \/ g is Element of bool the carrier of X

g \/ (f3 \/ g) is Element of bool the carrier of X

(g \/ (f3 \/ g)) /\ (v \/ f) is Element of bool the carrier of X

(f3 \/ g) /\ (v \/ f) is Element of bool the carrier of X

(g /\ (v \/ f)) \/ ((f3 \/ g) /\ (v \/ f)) is Element of bool the carrier of X

{} \/ ((f3 \/ g) /\ (v \/ f)) is set

(f3 /\ (v \/ f)) \/ (g /\ (v \/ f)) is Element of bool the carrier of X

the carrier of (f1 meet (Y union X1)) is non empty set

f \/ (v /\ f) is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

the topology of X 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

TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

Y meet X1 is non empty strict TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

X2 meet (Y union X1) is non empty strict TopSpace-like SubSpace of X

f1 is non empty TopSpace-like SubSpace of X

X2 union f1 is non empty strict TopSpace-like SubSpace of X

f1 meet (Y union X1) is non empty strict TopSpace-like SubSpace of X

f2 is non empty TopSpace-like SubSpace of X

(X2 union f1) union f2 is non empty strict TopSpace-like SubSpace of X

f2 meet (Y union X1) is non empty strict TopSpace-like SubSpace of X

the carrier of f2 is non empty set

the carrier of f1 is non empty set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

the carrier of Y is non empty set

the carrier of (X2 union f1) is non empty set

g is Element of bool the carrier of X

f3 is Element of bool the carrier of X

g \/ f3 is Element of bool the carrier of X

the carrier of (Y union X1) is non empty set

v is Element of bool the carrier of X

f is Element of bool the carrier of X

v \/ f is Element of bool the carrier of X

g is Element of bool the carrier of X

(g \/ f3) \/ g is Element of bool the carrier of X

((g \/ f3) \/ g) /\ (v \/ f) is Element of bool the carrier of X

(g \/ f3) /\ (v \/ f) is Element of bool the carrier of X

g /\ (v \/ f) is Element of bool the carrier of X

((g \/ f3) /\ (v \/ f)) \/ (g /\ (v \/ f)) is Element of bool the carrier of X

((g \/ f3) /\ (v \/ f)) \/ {} is set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X2 is non empty set

the carrier of Y is non empty set

the carrier of X1 is non empty set

f2 is Element of bool the carrier of X

f1 is Element of bool the carrier of X

g is Element of bool the carrier of X

f2 /\ f1 is Element of bool the carrier of X

g /\ f1 is Element of bool the carrier of X

(f2 /\ f1) \/ (g /\ f1) is Element of bool the carrier of X

f2 \/ g is Element of bool the carrier of X

(f2 \/ g) /\ f1 is Element of bool the carrier of X

the carrier of (Y union X1) is non empty set

the carrier of (Y union X1) /\ f1 is Element of bool the carrier of X

the carrier of (Y union X1) is non empty set

f1 is Element of bool the carrier of X

the carrier of (Y union X1) /\ f1 is Element of bool the carrier of X

f2 is Element of bool the carrier of X

g is Element of bool the carrier of X

f2 \/ g is Element of bool the carrier of X

(f2 \/ g) /\ f1 is Element of bool the carrier of X

f2 /\ f1 is Element of bool the carrier of X

g /\ f1 is Element of bool the carrier of X

(f2 /\ f1) \/ (g /\ f1) is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X2 is non empty set

the carrier of Y is non empty set

the carrier of X1 is non empty set

the carrier of (Y union X1) is non empty set

f1 is Element of bool the carrier of X

the carrier of (Y union X1) /\ f1 is Element of bool the carrier of X

f2 is Element of bool the carrier of X

g is Element of bool the carrier of X

f2 \/ g is Element of bool the carrier of X

(f2 \/ g) /\ f1 is Element of bool the carrier of X

f2 /\ f1 is Element of bool the carrier of X

g /\ f1 is Element of bool the carrier of X

(f2 /\ f1) \/ (g /\ f1) is Element of bool the carrier of X

f2 is Element of bool the carrier of X

f1 is Element of bool the carrier of X

f2 /\ f1 is Element of bool the carrier of X

g is Element of bool the carrier of X

g /\ f1 is Element of bool the carrier of X

(f2 /\ f1) \/ (g /\ f1) is Element of bool the carrier of X

f2 \/ g is Element of bool the carrier of X

(f2 \/ g) /\ f1 is Element of bool the carrier of X

the carrier of (Y union X1) is non empty set

the carrier of (Y union X1) /\ f1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y meet X1 is non empty strict TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X2 is non empty set

the carrier of Y is non empty set

the carrier of X1 is non empty set

the carrier of (Y meet X1) is non empty set

f1 is Element of bool the carrier of X

the carrier of (Y meet X1) /\ f1 is Element of bool the carrier of X

f2 is Element of bool the carrier of X

g is Element of bool the carrier of X

f2 /\ g is Element of bool the carrier of X

(f2 /\ g) /\ f1 is Element of bool the carrier of X

f1 /\ f1 is Element of bool the carrier of X

g /\ (f1 /\ f1) is Element of bool the carrier of X

f2 /\ (g /\ (f1 /\ f1)) is Element of bool the carrier of X

g /\ f1 is Element of bool the carrier of X

f1 /\ (g /\ f1) is Element of bool the carrier of X

f2 /\ (f1 /\ (g /\ f1)) is Element of bool the carrier of X

f2 /\ f1 is Element of bool the carrier of X

(f2 /\ f1) /\ (g /\ f1) is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y meet X1 is non empty strict TopSpace-like SubSpace of X

X2 is non empty TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X2 is non empty set

the carrier of Y is non empty set

the carrier of X1 is non empty set

f2 is Element of bool the carrier of X

f1 is Element of bool the carrier of X

g is Element of bool the carrier of X

f2 /\ f1 is Element of bool the carrier of X

g /\ f1 is Element of bool the carrier of X

(f2 /\ f1) /\ (g /\ f1) is Element of bool the carrier of X

(g /\ f1) /\ f1 is Element of bool the carrier of X

f2 /\ ((g /\ f1) /\ f1) is Element of bool the carrier of X

f1 /\ f1 is Element of bool the carrier of X

g /\ (f1 /\ f1) is Element of bool the carrier of X

f2 /\ (g /\ (f1 /\ f1)) is Element of bool the carrier of X

f2 /\ g is Element of bool the carrier of X

(f2 /\ g) /\ f1 is Element of bool the carrier of X

the carrier of (Y meet X1) is non empty set

the carrier of (Y meet X1) /\ f1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like closed SubSpace of X

X1 meet Y is non empty strict TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X1 is non empty set

the carrier of Y is non empty set

bool the carrier of Y is non empty set

X2 is Element of bool the carrier of X

f1 is Element of bool the carrier of X

X2 /\ f1 is Element of bool the carrier of X

f2 is Element of bool the carrier of Y

[#] Y is non empty non proper open closed Element of bool the carrier of Y

X2 /\ ([#] Y) is Element of bool the carrier of Y

the carrier of (X1 meet Y) is non empty set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like open SubSpace of X

X1 meet Y is non empty strict TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X1 is non empty set

the carrier of Y is non empty set

bool the carrier of Y is non empty set

X2 is Element of bool the carrier of X

f1 is Element of bool the carrier of X

X2 /\ f1 is Element of bool the carrier of X

f2 is Element of bool the carrier of Y

[#] Y is non empty non proper open closed Element of bool the carrier of Y

X2 /\ ([#] Y) is Element of bool the carrier of Y

the carrier of (X1 meet Y) is non empty set

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

X1 union Y is non empty strict TopSpace-like SubSpace of X

the carrier of Y is non empty set

the topology of Y is non empty Element of bool (bool the carrier of Y)

bool the carrier of Y is non empty set

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

TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct

f1 is non empty TopSpace-like closed SubSpace of X

f1 meet (Y union X1) is non empty strict TopSpace-like SubSpace of X

X2 is TopSpace-like SubSpace of X

X is non empty TopSpace-like TopStruct

Y is non empty TopSpace-like SubSpace of X

X1 is non empty TopSpace-like SubSpace of X

Y union X1 is non empty strict TopSpace-like SubSpace of X

X1 union Y is non empty strict TopSpace-like SubSpace of X

the carrier of Y is non empty set

the topology of Y is non empty Element of bool (bool the carrier of Y)

bool the carrier of Y is non empty set

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

TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct

f1 is non empty TopSpace-like open SubSpace of X

f1 meet (Y union X1) is non empty strict TopSpace-like SubSpace of X

X2 is TopSpace-like SubSpace of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

[: the carrier of X, the carrier of Y:] is non empty Relation-like set

bool [: the carrier of X, the carrier of Y:] is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

[: the carrier of X, the carrier of Y:] is non empty Relation-like set

bool [: the carrier of X, the carrier of Y:] is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

[: the carrier of Y, the carrier of X:] is non empty Relation-like set

bool [: the carrier of Y, the carrier of X:] is non empty set

X1 is non empty Relation-like the carrier of Y -defined the carrier of X -valued Function-like total V21( the carrier of Y, the carrier of X) Element of bool [: the carrier of Y, the carrier of X:]

X2 is Element of the carrier of Y

X1 . X2 is Element of the carrier of X

f1 is a_neighborhood of X1 . X2

X1 " f1 is Element of bool the carrier of Y

bool the carrier of Y is non empty set

f2 is a_neighborhood of X2

X1 .: f2 is Element of bool the carrier of X

bool the carrier of X is non empty set

g is Element of bool the carrier of Y

g is Element of bool the carrier of Y

f1 is a_neighborhood of X1 . X2

X1 " f1 is Element of bool the carrier of Y

bool the carrier of Y is non empty set

f2 is a_neighborhood of X2

X1 .: f2 is Element of bool the carrier of X

bool the carrier of X 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

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

[: the carrier of X, the carrier of Y:] is non empty Relation-like set

bool [: the carrier of X, the carrier of Y:] is non empty set

bool the carrier of Y is non empty set

X1 is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total V21( the carrier of X, the carrier of Y) Element of bool [: the carrier of X, the carrier of Y:]

X2 is Element of the carrier of X

X1 . X2 is Element of the carrier of Y

f1 is Element of bool the carrier of Y

f2 is a_neighborhood of X1 . X2

g is a_neighborhood of X2

X1 .: g is Element of bool the carrier of Y

f3 is Element of bool the carrier of X

X1 .: f3 is Element of bool the carrier of Y

f1 is a_neighborhood of X1 . X2

f2 is Element of bool the carrier of Y

g is Element of bool the carrier of X

X1 .: g is Element of bool the carrier of Y

f3 is a_neighborhood of X2

X1 .: f3 is Element of bool the carrier of Y

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

[: the carrier of Y, the carrier of X:] is non empty Relation-like set

bool [: the carrier of Y, the carrier of X:] is non empty set

X1 is non empty Relation-like the carrier of Y -defined the carrier of X -valued Function-like total V21( the carrier of Y, the carrier of X) Element of bool [: the carrier of Y, the carrier of X:]

X2 is Element of the carrier of Y

X1 . X2 is Element of the carrier of X

f1 is a_neighborhood of X1 . X2

X2 is Element of the carrier of Y

X1 . X2 is Element of the carrier of X

f1 is a_neighborhood of X1 . X2

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

the topology of X1 is non empty Element of bool (bool the carrier of X1)

bool the carrier of X1 is non empty set

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

the topology of Y is non empty Element of bool (bool the carrier of Y)

bool the carrier of Y is non empty set

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

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

[: the carrier of X, the carrier of Y:] is non empty Relation-like set

bool [: the carrier of X, the carrier of Y:] is non empty set

[: the carrier of X, the carrier of X1:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X1:] is non empty set

X2 is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total V21( the carrier of X, the carrier of Y) Element of bool [: the carrier of X, the carrier of Y:]

f1 is non empty Relation-like the carrier of X -defined the carrier of X1 -valued Function-like total V21( the carrier of X, the carrier of X1) Element of bool [: the carrier of X, the carrier of X1:]

f2 is Element of the carrier of X

f1 . f2 is Element of the carrier of X1

bool the carrier of X is non empty set

g is Element of bool the carrier of X1

f3 is Element of bool the carrier of Y

g is Element of bool the carrier of X

X2 .: g is Element of bool the carrier of Y

f1 .: g is Element of bool the carrier of X1

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

the topology of Y is non empty Element of bool (bool the carrier of Y)

bool the carrier of Y is non empty set

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

the topology of X 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

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

[: the carrier of X, the carrier of X1:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X1:] is non empty set

[: the carrier of Y, the carrier of X1:] is non empty Relation-like set

bool [: the carrier of Y, the carrier of X1:] is non empty set

X2 is non empty Relation-like the carrier of X -defined the carrier of X1 -valued Function-like total V21( the carrier of X, the carrier of X1) Element of bool [: the carrier of X, the carrier of X1:]

f1 is non empty Relation-like the carrier of Y -defined the carrier of X1 -valued Function-like total V21( the carrier of Y, the carrier of X1) Element of bool [: the carrier of Y, the carrier of X1:]

f2 is Element of the carrier of X

g is Element of the carrier of Y

bool the carrier of X1 is non empty set

X2 . f2 is Element of the carrier of X1

f3 is Element of bool the carrier of X1

g is Element of bool the carrier of Y

f1 .: g is Element of bool the carrier of X1

f is Element of bool the carrier of X

X2 .: f is Element of bool the carrier of X1

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

[: the carrier of Y, the carrier of X1:] is non empty Relation-like set

bool [: the carrier of Y, the carrier of X1:] is non empty set

[: the carrier of X1, the carrier of X:] is non empty Relation-like set

bool [: the carrier of X1, the carrier of X:] is non empty set

X2 is non empty Relation-like the carrier of Y -defined the carrier of X1 -valued Function-like total V21( the carrier of Y, the carrier of X1) Element of bool [: the carrier of Y, the carrier of X1:]

f1 is non empty Relation-like the carrier of X1 -defined the carrier of X -valued Function-like total V21( the carrier of X1, the carrier of X) Element of bool [: the carrier of X1, the carrier of X:]

f1 * X2 is non empty Relation-like the carrier of Y -defined the carrier of X -valued Function-like total V21( the carrier of Y, the carrier of X) Element of bool [: the carrier of Y, the carrier of X:]

[: the carrier of Y, the carrier of X:] is non empty Relation-like set

bool [: the carrier of Y, the carrier of X:] is non empty set

f2 is Element of the carrier of Y

X2 . f2 is Element of the carrier of X1

g is Element of the carrier of X1

(f1 * X2) . f2 is Element of the carrier of X

f3 is a_neighborhood of (f1 * X2) . f2

(f1 * X2) " f3 is Element of bool the carrier of Y

bool the carrier of Y is non empty set

f1 . g is Element of the carrier of X

f1 " f3 is Element of bool the carrier of X1

bool the carrier of X1 is non empty set

X2 " (f1 " f3) is Element of bool the carrier of Y

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

[: the carrier of Y, the carrier of X:] is non empty Relation-like set

bool [: the carrier of Y, the carrier of X:] is non empty set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

[: the carrier of X1, the carrier of Y:] is non empty Relation-like set

bool [: the carrier of X1, the carrier of Y:] is non empty set

X2 is non empty Relation-like the carrier of X1 -defined the carrier of Y -valued Function-like total V21( the carrier of X1, the carrier of Y) Element of bool [: the carrier of X1, the carrier of Y:]

f1 is non empty Relation-like the carrier of Y -defined the carrier of X -valued Function-like total V21( the carrier of Y, the carrier of X) Element of bool [: the carrier of Y, the carrier of X:]

f1 * X2 is non empty Relation-like the carrier of X1 -defined the carrier of X -valued Function-like total V21( the carrier of X1, the carrier of X) Element of bool [: the carrier of X1, the carrier of X:]

[: the carrier of X1, the carrier of X:] is non empty Relation-like set

bool [: the carrier of X1, the carrier of X:] is non empty set

f2 is Element of the carrier of Y

{f2} is non empty Element of bool the carrier of Y

bool the carrier of Y is non empty set

X2 " {f2} is Element of bool the carrier of X1

bool the carrier of X1 is non empty set

g is Element of the carrier of X1

{g} is non empty Element of bool the carrier of X1

bool (X2 " {f2}) is non empty set

dom X2 is non empty Element of bool the carrier of X1

[#] X1 is non empty non proper open closed Element of bool the carrier of X1

Im (X2,g) is set

{g} is non empty set

X2 .: {g} is set

X2 . g is Element of the carrier of Y

{(X2 . g)} is non empty Element of bool the carrier of Y

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

[: the carrier of X, the carrier of Y:] is non empty Relation-like set

bool [: the carrier of X, the carrier of Y:] is non empty set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

[: the carrier of X1, the carrier of X:] is non empty Relation-like set

bool [: the carrier of X1, the carrier of X:] is non empty set

X2 is non empty Relation-like the carrier of X1 -defined the carrier of X -valued Function-like total V21( the carrier of X1, the carrier of X) Element of bool [: the carrier of X1, the carrier of X:]

f1 is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total V21( the carrier of X, the carrier of Y) Element of bool [: the carrier of X, the carrier of Y:]

f1 * X2 is non empty Relation-like the carrier of X1 -defined the carrier of Y -valued Function-like total V21( the carrier of X1, the carrier of Y) Element of bool [: the carrier of X1, the carrier of Y:]

[: the carrier of X1, the carrier of Y:] is non empty Relation-like set

bool [: the carrier of X1, the carrier of Y:] is non empty set

f2 is Element of the carrier of X1

X2 . f2 is Element of the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

[: the carrier of X, the carrier of Y:] is non empty Relation-like set

bool [: the carrier of X, the carrier of Y:] is non empty set

f1 is non empty TopSpace-like TopStruct

the carrier of f1 is non empty set

f2 is non empty TopSpace-like TopStruct

the carrier of f2 is non empty set

[: the carrier of f1, the carrier of f2:] is non empty Relation-like set

bool [: the carrier of f1, the carrier of f2:] is non empty set

X1 is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total V21( the carrier of X, the carrier of Y) Element of bool [: the carrier of X, the carrier of Y:]

X2 is Element of the carrier of X

g is non empty Relation-like the carrier of f1 -defined the carrier of f2 -valued Function-like total V21( the carrier of f1, the carrier of f2) Element of bool [: the carrier of f1, the carrier of f2:]

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

the topology of X1 is non empty Element of bool (bool the carrier of X1)

bool the carrier of X1 is non empty set

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

the topology of Y is non empty Element of bool (bool the carrier of Y)

bool the carrier of Y is non empty set

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

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

[: the carrier of X, the carrier of Y:] is non empty Relation-like set

bool [: the carrier of X, the carrier of Y:] is non empty set

[: the carrier of X, the carrier of X1:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X1:] is non empty set

X2 is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total V21( the carrier of X, the carrier of Y) continuous Element of bool [: the carrier of X, the carrier of Y:]

f1 is non empty Relation-like the carrier of X -defined the carrier of X1 -valued Function-like total V21( the carrier of X, the carrier of X1) Element of bool [: the carrier of X, the carrier of X1:]

f2 is Element of the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

the topology of Y is non empty Element of bool (bool the carrier of Y)

bool the carrier of Y is non empty set

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

the topology of X 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

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

[: the carrier of Y, the carrier of X1:] is non empty Relation-like set

bool [: the carrier of Y, the carrier of X1:] is non empty set

[: the carrier of X, the carrier of X1:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X1:] is non empty set

X2 is non empty Relation-like the carrier of Y -defined the carrier of X1 -valued Function-like total V21( the carrier of Y, the carrier of X1) continuous Element of bool [: the carrier of Y, the carrier of X1:]

f1 is non empty Relation-like the carrier of X -defined the carrier of X1 -valued Function-like total V21( the carrier of X, the carrier of X1) Element of bool [: the carrier of X, the carrier of X1:]

f2 is Element of the carrier of X

g is Element of the carrier of Y

X is set

[:X,{}:] is Relation-like set

bool [:X,{}:] is non empty set

Y is empty Relation-like non-empty empty-yielding X -defined {} -valued Function-like one-to-one constant functional Element of bool [:X,{}:]

X is 1-sorted

the carrier of X is set

Y is 1-sorted

the carrier of Y is set

[: the carrier of X, the carrier of Y:] is Relation-like set

bool [: the carrier of X, the carrier of Y:] is non empty set

X2 is 1-sorted

the carrier of X2 is set

X1 is Relation-like the carrier of X -defined the carrier of Y -valued Function-like V21( the carrier of X, the carrier of Y) Element of bool [: the carrier of X, the carrier of Y:]

X1 | the carrier of X2 is Relation-like the carrier of X -defined the carrier of X2 -defined the carrier of X -defined the carrier of Y -valued Function-like Element of bool [: the carrier of X, the carrier of Y:]

[: the carrier of X2, the carrier of Y:] is Relation-like set

bool [: the carrier of X2, the carrier of Y:] is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty set

[: the carrier of X, the carrier of Y:] is non empty Relation-like set

bool [: the carrier of X, the carrier of Y:] is non empty set

X2 is TopSpace-like SubSpace of X

the carrier of X2 is set

[: the carrier of X2, the carrier of Y:] is Relation-like set

bool [: the carrier of X2, the carrier of Y:] is non empty set

X1 is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total V21( the carrier of X, the carrier of Y) Element of bool [: the carrier of X, the carrier of Y:]

(X,Y,X1,X2) is Relation-like the carrier of X2 -defined the carrier of Y -valued Function-like total V21( the carrier of X2, the carrier of Y) Element of bool [: the carrier of X2, the carrier of Y:]

X1 | the carrier of X2 is Relation-like the carrier of X -defined the carrier of X2 -defined the carrier of X -defined the carrier of Y -valued Function-like Element of bool [: the carrier of X, the carrier of Y:]

[#] X2 is non proper open closed Element of bool the carrier of X2

bool the carrier of X2 is non empty set

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

bool the carrier of X is non empty set

f1 is Relation-like the carrier of X2 -defined the carrier of Y -valued Function-like total V21( the carrier of X2, the carrier of Y) Element of bool [: the carrier of X2, the carrier of Y:]

f2 is Relation-like the carrier of X2 -defined the carrier of Y -valued Function-like total V21( the carrier of X2, the carrier of Y) Element of bool [: the carrier of X2, the carrier of Y:]

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

Y is non empty TopSpace-like TopStruct

the carrier of Y is non empty