:: 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₁₇ is set
g2 is Relation-like f2 /\ f1 -defined Y -valued Function-like total V21(f2 /\ f1,Y) Element of bool [:(f2 /\ f1),Y:]
g2 . c₁₇ is set
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₁₇ is set
v | (X1 /\ f1) is Relation-like X1 /\ f1 -defined f2 -defined Y -valued Function-like Element of bool [:f2,Y:]
(v | (X1 /\ f1)) . c₁₇ is set
(f | (X1 /\ f1)) . c₁₇ is set
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₁₇ is set
F . c₁₇ is set
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₁₇ is set
v | (X2 /\ f1) is Relation-like X2 /\ f1 -defined f2 -defined Y -valued Function-like Element of bool [:f2,Y:]
(v | (X2 /\ f1)) . c₁₇ is set
(f | (X2 /\ f1)) . c₁₇ is set
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₁₇ is set
(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₁₇ is set
G is non empty Relation-like g -defined Y -valued Function-like total V21(g,Y) Element of bool [:g,Y:]
G . c₁₇ is set
g1 . c₁₇ is set
g . c₁₇ is set
a | X2 is Relation-like X2 -defined g -defined Y -valued Function-like Element of bool [:g,Y:]
(a | X2) . c₁₇ is set
a . c₁₇ is set
g1 | f1 is Relation-like f1 -defined X1 \/ g -defined Y -valued Function-like Element of bool [:(X1 \/ g),Y:]
(g1 | f1) . c₁₇ is set
f . c₁₇ is set
a | f1 is Relation-like f1 -defined g -defined Y -valued Function-like Element of bool [:g,Y:]
(a | f1) . c₁₇ is set
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