:: BORSUK_1 semantic presentation

REAL is V29() V30() V31() V35() set
NAT is V29() V30() V31() V32() V33() V34() V35() Element of bool REAL
bool REAL is non empty set

1 is non empty V29() V30() V31() V32() V33() V34() natural real ext-real positive Element of NAT
{{},1} is non empty finite set
omega is V29() V30() V31() V32() V33() V34() V35() set
bool omega is non empty set
[:1,1:] is non empty Relation-like set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like set
bool [:[:1,1:],1:] is non empty set

bool [:[:1,1:],REAL:] is non empty set

bool is non empty set
2 is non empty V29() V30() V31() V32() V33() V34() natural real ext-real positive Element of NAT
[:2,2:] is non empty Relation-like set

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

r is TopStruct
the carrier of r is set
X is SubSpace of r
the carrier of X is set
[#] X is non proper dense Element of bool the carrier of X
bool the carrier of X is non empty set
[#] r is non proper dense Element of bool the carrier of r
bool the carrier of r is non empty set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
bool [: the carrier of r, the carrier of X:] is non empty set
D is non empty Relation-like the carrier of r -defined the carrier of X -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of X) Element of bool [: the carrier of r, the carrier of X:]
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
bool the carrier of X is non empty set
CH1 is Element of the carrier of r
D . CH1 is Element of the carrier of X
II is a_neighborhood of D . CH1
Int II is open Element of bool the carrier of X
D " (Int II) is Element of bool the carrier of r
bool the carrier of r is non empty set
Int (D " (Int II)) is open Element of bool the carrier of r
THETA is a_neighborhood of CH1
D .: THETA is Element of bool the carrier of X
D " II is Element of bool the carrier of r
CH1 is Element of bool the carrier of X
II is set
D " CH1 is Element of bool the carrier of r
bool the carrier of r is non empty set
Int CH1 is open Element of bool the carrier of X
THETA is Element of the carrier of r
D . THETA is Element of the carrier of X
THETA is a_neighborhood of THETA
D .: THETA is Element of bool the carrier of X
Int THETA is open Element of bool the carrier of r
dom D is non empty Element of bool the carrier of r
D " (D .: THETA) is Element of bool the carrier of r
THETA is Element of bool the carrier of r
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
bool [: the carrier of r, the carrier of X:] is non empty set
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
[: the carrier of X, the carrier of D:] is non empty Relation-like set
bool [: the carrier of X, the carrier of D:] is non empty set
[: the carrier of r, the carrier of D:] is non empty Relation-like set
bool [: the carrier of r, the carrier of D:] is non empty set
CH1 is non empty Relation-like the carrier of r -defined the carrier of X -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of X) continuous Element of bool [: the carrier of r, the carrier of X:]
II is non empty Relation-like the carrier of X -defined the carrier of D -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of D) continuous Element of bool [: the carrier of X, the carrier of D:]
II * CH1 is non empty Relation-like the carrier of r -defined the carrier of D -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of D) Element of bool [: the carrier of r, the carrier of D:]
THETA is non empty Relation-like the carrier of r -defined the carrier of D -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of D) Element of bool [: the carrier of r, the carrier of D:]
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
bool [: the carrier of r, the carrier of X:] is non empty set
bool the carrier of X is non empty set
D is non empty Relation-like the carrier of r -defined the carrier of X -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of X) continuous Element of bool [: the carrier of r, the carrier of X:]
CH1 is Element of bool the carrier of X
Int CH1 is open Element of bool the carrier of X
D " (Int CH1) is Element of bool the carrier of r
bool the carrier of r is non empty set
D " CH1 is Element of bool the carrier of r
Int (D " CH1) is open Element of bool the carrier of r
II is set
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
r is non empty TopSpace-like TopStruct
the carrier of r 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 r:] is non empty Relation-like set
bool [: the carrier of X, the carrier of r:] is non empty set
D is Element of the carrier of r
{D} is non empty trivial finite Element of bool the carrier of r
bool the carrier of r is non empty set
CH1 is non empty Relation-like the carrier of X -defined the carrier of r -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of r) continuous Element of bool [: the carrier of X, the carrier of r:]
CH1 " {D} is Element of bool the carrier of X
bool the carrier of X is non empty set
II is a_neighborhood of D
CH1 " II is Element of bool the carrier of X
Int II is open Element of bool the carrier of r
CH1 " (Int II) is Element of bool the carrier of X
Int (CH1 " II) is open Element of bool the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
bool [: the carrier of r, the carrier of X:] is non empty set
D is Element of the carrier of X
CH1 is non empty Relation-like the carrier of r -defined the carrier of X -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of X) continuous Element of bool [: the carrier of r, the carrier of X:]
II is a_neighborhood of D
CH1 " II is set
{D} is non empty trivial finite Element of bool the carrier of X
bool the carrier of X is non empty set
CH1 " {D} is Element of bool the carrier of r
bool the carrier of r is non empty set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
bool the carrier of r is non empty set
D is Element of bool the carrier of r
X is Element of bool the carrier of r
CH1 is a_neighborhood of D
Int CH1 is open Element of bool the carrier of r
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
bool the carrier of r is non empty set
X is Element of the carrier of r
{X} is non empty trivial finite Element of bool the carrier of r
bool (bool the carrier of r) is non empty set
CH1 is Element of bool (bool the carrier of r)
D is Element of bool the carrier of r
union CH1 is Element of bool the carrier of r
II is set
{II} is non empty trivial finite set
THETA is Element of bool (bool the carrier of r)
THETA is Element of bool (bool the carrier of r)
union THETA is Element of bool the carrier of r
CH1 is Element of bool the carrier of r

the carrier of r is set

the carrier of X is set
[: the carrier of r, the carrier of X:] is Relation-like set
bool the carrier of r is non empty set
bool the carrier of X is non empty set
the topology of r is non empty Element of bool (bool the carrier of r)
bool (bool the carrier of r) is non empty set
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ [:b1,b2:] where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( b1 in the topology of r & b2 in the topology of X ) } is set
bool [: the carrier of r, the carrier of X:] is non empty set
bool (bool [: the carrier of r, the carrier of X:]) is non empty set
{ (union b1) where b1 is Element of bool (bool [: the carrier of r, the carrier of X:]) : b1 c= { [:b1,b2:] where b2 is Element of bool the carrier of r, b3 is Element of bool the carrier of X : ( b1 in the topology of r & b2 in the topology of X ) } } is set
bool [: the carrier of r, the carrier of X:] is non empty Element of bool (bool [: the carrier of r, the carrier of X:])
CH1 is set
II is Element of bool (bool [: the carrier of r, the carrier of X:])
union II is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
CH1 is Element of bool (bool [: the carrier of r, the carrier of X:])
TopStruct(# [: the carrier of r, the carrier of X:],CH1 #) is strict TopStruct
{[: the carrier of r, the carrier of X:]} is non empty trivial finite set
THETA is Element of bool (bool [: the carrier of r, the carrier of X:])
THETA is Element of bool (bool [: the carrier of r, the carrier of X:])
THETA9 is set
the carrier of TopStruct(# [: the carrier of r, the carrier of X:],CH1 #) is set
union THETA is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
the topology of TopStruct(# [: the carrier of r, the carrier of X:],CH1 #) is Element of bool (bool the carrier of TopStruct(# [: the carrier of r, the carrier of X:],CH1 #))
bool the carrier of TopStruct(# [: the carrier of r, the carrier of X:],CH1 #) is non empty set
bool (bool the carrier of TopStruct(# [: the carrier of r, the carrier of X:],CH1 #)) is non empty set
THETA9 is Element of bool (bool the carrier of TopStruct(# [: the carrier of r, the carrier of X:],CH1 #))
union THETA9 is Element of bool the carrier of TopStruct(# [: the carrier of r, the carrier of X:],CH1 #)
{ [:b1,b2:] where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( b1 in the topology of r & b2 in the topology of X & ex b3 being set st
( b3 in THETA9 & [:b1,b2:] c= b3 ) )
}
is set

W is set
W9 is Element of bool the carrier of r
T is Element of bool the carrier of X
[:W9,T:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
T is set
W is Element of bool (bool [: the carrier of r, the carrier of X:])
union W is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
W9 is set
T is set
[W9,T] is non empty V7() set
{W9,T} is non empty finite set
{W9} is non empty trivial finite set
{{W9,T},{W9}} is non empty finite V28() set
T is set
GG is Element of bool the carrier of r
U is Element of bool the carrier of X
[:GG,U:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
V is set
W9 is set
T is set
T is Element of bool (bool [: the carrier of r, the carrier of X:])
union T is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
GG is set
U is Element of bool the carrier of r
V is Element of bool the carrier of X
[:U,V:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
W9 is set
T is Element of bool the carrier of r
T is Element of bool the carrier of X
[:T,T:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
GG is set
THETA9 is Element of bool the carrier of TopStruct(# [: the carrier of r, the carrier of X:],CH1 #)
THETA99 is Element of bool the carrier of TopStruct(# [: the carrier of r, the carrier of X:],CH1 #)
THETA9 /\ THETA99 is Element of bool the carrier of TopStruct(# [: the carrier of r, the carrier of X:],CH1 #)
{ [:b1,b2:] where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( b1 in the topology of r & b2 in the topology of X & [:b1,b2:] c= THETA9 /\ THETA99 ) } is set
W9 is set
T is Element of bool the carrier of r
T is Element of bool the carrier of X
[:T,T:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
T is Element of bool (bool [: the carrier of r, the carrier of X:])
union T is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
T is Element of bool (bool [: the carrier of r, the carrier of X:])
union T is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
W9 is Element of bool (bool [: the carrier of r, the carrier of X:])
union W9 is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
GG is set
U is set
V is set
H9 is Element of bool the carrier of r
H99 is Element of bool the carrier of X
[:H9,H99:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
H is Element of bool the carrier of r
Y2 is Element of bool the carrier of X
[:H,Y2:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
[:H9,H99:] /\ [:H,Y2:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
H9 /\ H is Element of bool the carrier of r
H99 /\ Y2 is Element of bool the carrier of X
[:(H9 /\ H),(H99 /\ Y2):] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
GG is set
U is set
[GG,U] is non empty V7() set
{GG,U} is non empty finite set
{GG} is non empty trivial finite set
{{GG,U},{GG}} is non empty finite V28() set
V is set
H9 is Element of bool the carrier of r
H99 is Element of bool the carrier of X
[:H9,H99:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
GG is set
U is Element of bool the carrier of r
V is Element of bool the carrier of X
[:U,V:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
THETA is strict TopSpace-like TopStruct
the carrier of THETA is set
the topology of THETA is non empty Element of bool (bool the carrier of THETA)
bool the carrier of THETA is non empty set
bool (bool the carrier of THETA) is non empty set
{ (union b1) where b1 is Element of bool (bool the carrier of THETA) : b1 c= { [:b1,b2:] where b2 is Element of bool the carrier of r, b3 is Element of bool the carrier of X : ( b1 in the topology of r & b2 in the topology of X ) } } is set

the carrier of D is set
the topology of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
{ (union b1) where b1 is Element of bool (bool the carrier of D) : b1 c= { [:b1,b2:] where b2 is Element of bool the carrier of r, b3 is Element of bool the carrier of X : ( b1 in the topology of r & b2 in the topology of X ) } } is set

the carrier of CH1 is set
the topology of CH1 is non empty Element of bool (bool the carrier of CH1)
bool the carrier of CH1 is non empty set
bool (bool the carrier of CH1) is non empty set
{ (union b1) where b1 is Element of bool (bool the carrier of CH1) : b1 c= { [:b1,b2:] where b2 is Element of bool the carrier of r, b3 is Element of bool the carrier of X : ( b1 in the topology of r & b2 in the topology of X ) } } is set

(r,X) is strict TopSpace-like TopStruct
the carrier of (r,X) is set
the carrier of r is set

[: the carrier of r, the carrier of X:] is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V28() V29() V30() V31() V32() V33() V34() V35() set
(X,r) is strict TopSpace-like TopStruct
the carrier of (X,r) is set

the carrier of r is set
[: the carrier of X, the carrier of r:] is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V28() V29() V30() V31() V32() V33() V34() V35() set
r is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
(r,X) is strict TopSpace-like TopStruct
the carrier of (r,X) is set
the carrier of r is non empty set
the carrier of X is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set

(r,X) is strict TopSpace-like TopStruct
the carrier of (r,X) is set
bool the carrier of (r,X) is non empty set
bool (bool the carrier of (r,X)) is non empty set
the carrier of r is set
bool the carrier of r is non empty set
the carrier of X is set
bool the carrier of X is non empty set
D is Element of bool the carrier of (r,X)
the topology of (r,X) is non empty Element of bool (bool the carrier of (r,X))
the topology of r is non empty Element of bool (bool the carrier of r)
bool (bool the carrier of r) is non empty set
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
{ [:b1,b2:] where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( b1 in the topology of r & b2 in the topology of X ) } is set
{ (union b1) where b1 is Element of bool (bool the carrier of (r,X)) : b1 c= { [:b1,b2:] where b2 is Element of bool the carrier of r, b3 is Element of bool the carrier of X : ( b1 in the topology of r & b2 in the topology of X ) } } is set
CH1 is Element of bool (bool the carrier of (r,X))
union CH1 is Element of bool the carrier of (r,X)
II is set
THETA is Element of bool the carrier of r
THETA is Element of bool the carrier of X
[:THETA,THETA:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
[: the carrier of r, the carrier of X:] is Relation-like set
bool [: the carrier of r, the carrier of X:] is non empty set
THETA99 is Element of bool the carrier of r
THETA9 is Element of bool the carrier of X
[:THETA99,THETA9:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
CH1 is Element of bool (bool the carrier of (r,X))
union CH1 is Element of bool the carrier of (r,X)
II is set
THETA is Element of bool the carrier of r
THETA is Element of bool the carrier of X
[:THETA,THETA:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
[: the carrier of r, the carrier of X:] is Relation-like set
bool [: the carrier of r, the carrier of X:] is non empty set

the carrier of r is set
bool the carrier of r is non empty set

the carrier of X is set
bool the carrier of X is non empty set
D is Element of bool the carrier of r
CH1 is Element of bool the carrier of X
[:D,CH1:] is Relation-like set
(r,X) is strict TopSpace-like TopStruct
the carrier of (r,X) is set
bool the carrier of (r,X) is non empty set
[:D,CH1:] is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
[: the carrier of r, the carrier of X:] is Relation-like set
bool [: the carrier of r, the carrier of X:] is non empty set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
D is Element of the carrier of r
CH1 is Element of the carrier of X
[D,CH1] is non empty V7() set
{D,CH1} is non empty finite set
{D} is non empty trivial finite set
{{D,CH1},{D}} is non empty finite V28() set
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
[D,CH1] is non empty V7() Element of [: the carrier of r, the carrier of X:]
[: the carrier of r, the carrier of X:] is non empty Relation-like set

the carrier of r is set
bool the carrier of r is non empty set

the carrier of X is set
bool the carrier of X is non empty set
(r,X) is strict TopSpace-like TopStruct
D is Element of bool the carrier of r
CH1 is Element of bool the carrier of X
(r,X,D,CH1) is Relation-like Element of bool the carrier of (r,X)
the carrier of (r,X) is set
bool the carrier of (r,X) is non empty set
bool (bool the carrier of (r,X)) is non empty set
{(r,X,D,CH1)} is non empty trivial finite Element of bool (bool the carrier of (r,X))
II is Element of bool (bool the carrier of (r,X))
THETA is set
THETA is Element of bool (bool the carrier of (r,X))
THETA9 is Element of bool the carrier of r
THETA99 is Element of bool the carrier of X
(r,X,THETA9,THETA99) is Relation-like Element of bool the carrier of (r,X)
union {(r,X,D,CH1)} is Element of bool the carrier of (r,X)

the carrier of r is set
bool the carrier of r is non empty set

the carrier of X is set
bool the carrier of X is non empty set
(r,X) is strict TopSpace-like TopStruct
D is Element of bool the carrier of r
Int D is open Element of bool the carrier of r
CH1 is Element of bool the carrier of X
(r,X,D,CH1) is Relation-like Element of bool the carrier of (r,X)
the carrier of (r,X) is set
bool the carrier of (r,X) is non empty set
Int (r,X,D,CH1) is open Element of bool the carrier of (r,X)
Int CH1 is open Element of bool the carrier of X
(r,X,(Int D),(Int CH1)) is Relation-like Element of bool the carrier of (r,X)
II is set
THETA is Element of bool the carrier of (r,X)
bool (bool the carrier of (r,X)) is non empty set
THETA is Element of bool (bool the carrier of (r,X))
union THETA is Element of bool the carrier of (r,X)
THETA9 is set
THETA99 is Element of bool the carrier of r
W is Element of bool the carrier of X
(r,X,THETA99,W) is Relation-like Element of bool the carrier of (r,X)
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
(r,X) is non empty strict TopSpace-like TopStruct
D is Element of the carrier of r
CH1 is Element of the carrier of X
(r,X,D,CH1) is non empty V7() Element of the carrier of (r,X)
the carrier of (r,X) is non empty set
{D,CH1} is non empty finite set
{D} is non empty trivial finite set
{{D,CH1},{D}} is non empty finite V28() set
II is a_neighborhood of D
THETA is a_neighborhood of CH1
(r,X,II,THETA) is Relation-like Element of bool the carrier of (r,X)
bool the carrier of (r,X) is non empty set
Int II is open Element of bool the carrier of r
bool the carrier of r is non empty set
Int THETA is open Element of bool the carrier of X
bool the carrier of X is non empty set
(r,X,(Int II),(Int THETA)) is Relation-like Element of bool the carrier of (r,X)
Int (r,X,II,THETA) is open Element of bool the carrier of (r,X)
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
bool the carrier of r 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
(r,X) is non empty strict TopSpace-like TopStruct
D is Element of bool the carrier of r
CH1 is Element of bool the carrier of X
(r,X,D,CH1) is Relation-like Element of bool the carrier of (r,X)
the carrier of (r,X) is non empty set
bool the carrier of (r,X) is non empty set
II is a_neighborhood of D
THETA is a_neighborhood of CH1
(r,X,II,THETA) is Relation-like Element of bool the carrier of (r,X)
Int II is open Element of bool the carrier of r
Int THETA is open Element of bool the carrier of X
(r,X,(Int II),(Int THETA)) is Relation-like Element of bool the carrier of (r,X)
Int (r,X,II,THETA) is open Element of bool the carrier of (r,X)
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
D is Element of the carrier of r
CH1 is Element of the carrier of X
II is a_neighborhood of D
THETA is a_neighborhood of CH1
[:II,THETA:] is Relation-like set
(r,X) is non empty strict TopSpace-like TopStruct
(r,X,D,CH1) is non empty V7() Element of the carrier of (r,X)
the carrier of (r,X) is non empty set
{D,CH1} is non empty finite set
{D} is non empty trivial finite set
{{D,CH1},{D}} is non empty finite V28() set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty TopSpace-like TopStruct
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
the carrier of X is non empty set
D is Element of the carrier of (r,X)
[: the carrier of r, the carrier of X:] is non empty Relation-like set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
bool the carrier of r is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
D is Element of bool the carrier of r
CH1 is Element of the carrier of X
II is a_neighborhood of D
THETA is a_neighborhood of CH1
[:II,THETA:] is Relation-like set
(r,X) is non empty strict TopSpace-like TopStruct
{CH1} is non empty trivial finite compact Element of bool the carrier of X
bool the carrier of X is non empty set
(r,X,D,{CH1}) is Relation-like Element of bool the carrier of (r,X)
the carrier of (r,X) is non empty set
bool the carrier of (r,X) is non empty set
(r,X,II,THETA) is Relation-like Element of bool the carrier of (r,X)

(r,X) is strict TopSpace-like TopStruct
the carrier of (r,X) is set
bool the carrier of (r,X) is non empty set
the carrier of r is set
bool the carrier of r is non empty set
the carrier of X is set
bool the carrier of X is non empty set
D is Element of bool the carrier of (r,X)
{ (r,X,b1,b2) where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( (r,X,b1,b2) c= D & b1 is open & b2 is open ) } is set
bool (bool the carrier of (r,X)) is non empty set
bool the carrier of (r,X) is non empty Element of bool (bool the carrier of (r,X))
II is set
THETA is Element of bool the carrier of r
THETA is Element of bool the carrier of X
(r,X,THETA,THETA) is Relation-like Element of bool the carrier of (r,X)

(r,X) is strict TopSpace-like TopStruct
the carrier of (r,X) is set
bool the carrier of (r,X) is non empty set
D is Element of bool the carrier of (r,X)
(r,X,D) is Element of bool (bool the carrier of (r,X))
bool (bool the carrier of (r,X)) is non empty set
the carrier of r is set
bool the carrier of r is non empty set
the carrier of X is set
bool the carrier of X is non empty set
{ (r,X,b1,b2) where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( (r,X,b1,b2) c= D & b1 is open & b2 is open ) } is set
CH1 is Element of bool the carrier of (r,X)
II is Element of bool the carrier of r
THETA is Element of bool the carrier of X
(r,X,II,THETA) is Relation-like Element of bool the carrier of (r,X)

(r,X) is strict TopSpace-like TopStruct
the carrier of (r,X) is set
bool the carrier of (r,X) is non empty set
D is Element of bool the carrier of (r,X)
CH1 is Element of bool the carrier of (r,X)
(r,X,D) is open Element of bool (bool the carrier of (r,X))
bool (bool the carrier of (r,X)) is non empty set
the carrier of r is set
bool the carrier of r is non empty set
the carrier of X is set
bool the carrier of X is non empty set
{ (r,X,b1,b2) where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( (r,X,b1,b2) c= D & b1 is open & b2 is open ) } is set
(r,X,CH1) is open Element of bool (bool the carrier of (r,X))
{ (r,X,b1,b2) where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( (r,X,b1,b2) c= CH1 & b1 is open & b2 is open ) } is set
II is set
THETA is Element of bool the carrier of r
THETA is Element of bool the carrier of X
(r,X,THETA,THETA) is Relation-like Element of bool the carrier of (r,X)

(r,X) is strict TopSpace-like TopStruct
the carrier of (r,X) is set
bool the carrier of (r,X) is non empty set
D is Element of bool the carrier of (r,X)
(r,X,D) is open Element of bool (bool the carrier of (r,X))
bool (bool the carrier of (r,X)) is non empty set
the carrier of r is set
bool the carrier of r is non empty set
the carrier of X is set
bool the carrier of X is non empty set
{ (r,X,b1,b2) where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( (r,X,b1,b2) c= D & b1 is open & b2 is open ) } is set
union (r,X,D) is Element of bool the carrier of (r,X)
CH1 is set
II is set
THETA is Element of bool the carrier of r
THETA is Element of bool the carrier of X
(r,X,THETA,THETA) is Relation-like Element of bool the carrier of (r,X)

(r,X) is strict TopSpace-like TopStruct
the carrier of (r,X) is set
bool the carrier of (r,X) is non empty set
D is Element of bool the carrier of (r,X)
(r,X,D) is open Element of bool (bool the carrier of (r,X))
bool (bool the carrier of (r,X)) is non empty set
the carrier of r is set
bool the carrier of r is non empty set
the carrier of X is set
bool the carrier of X is non empty set
{ (r,X,b1,b2) where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( (r,X,b1,b2) c= D & b1 is open & b2 is open ) } is set
union (r,X,D) is Element of bool the carrier of (r,X)
CH1 is Element of bool (bool the carrier of (r,X))
union CH1 is Element of bool the carrier of (r,X)
II is set
THETA is set
THETA is Element of bool the carrier of r
THETA9 is Element of bool the carrier of X
(r,X,THETA,THETA9) is Relation-like Element of bool the carrier of (r,X)

(r,X) is strict TopSpace-like TopStruct
the carrier of (r,X) is set
bool the carrier of (r,X) is non empty set
D is Element of bool the carrier of (r,X)
Int D is open Element of bool the carrier of (r,X)
(r,X,D) is open Element of bool (bool the carrier of (r,X))
bool (bool the carrier of (r,X)) is non empty set
the carrier of r is set
bool the carrier of r is non empty set
the carrier of X is set
bool the carrier of X is non empty set
{ (r,X,b1,b2) where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( (r,X,b1,b2) c= D & b1 is open & b2 is open ) } is set
union (r,X,D) is Element of bool the carrier of (r,X)
(r,X,(Int D)) is open Element of bool (bool the carrier of (r,X))
{ (r,X,b1,b2) where b1 is Element of bool the carrier of r, b2 is Element of bool the carrier of X : ( (r,X,b1,b2) c= Int D & b1 is open & b2 is open ) } is set
union (r,X,(Int D)) is Element of bool the carrier of (r,X)
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
pr1 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of r -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of r) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of r:]
[:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty set
.: (pr1 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of r -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of r) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):]
bool [: the carrier of r, the carrier of X:] is non empty set
bool the carrier of r is non empty set
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty set
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
bool the carrier of (r,X) is non empty Element of bool (bool the carrier of (r,X))
bool the carrier of (r,X) is non empty set
bool (bool the carrier of (r,X)) is non empty set
bool the carrier of r is non empty Element of bool (bool the carrier of r)
bool (bool the carrier of r) is non empty set
[:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty set
pr2 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of X -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of X:]
[:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty set
.: (pr2 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of X -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of X) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):]
bool the carrier of X is non empty set
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
[:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
bool the carrier of r is non empty set
bool the carrier of r is non empty Element of bool (bool the carrier of r)
bool (bool the carrier of r) is non empty set
X is non empty TopSpace-like TopStruct
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
bool the carrier of (r,X) is non empty set
bool (bool the carrier of (r,X)) is non empty set
the carrier of X is non empty set
bool the carrier of X is non empty set
bool the carrier of (r,X) is non empty Element of bool (bool the carrier of (r,X))
(r,X) is non empty Relation-like bool the carrier of (r,X) -defined bool the carrier of r -valued Function-like V20( bool the carrier of (r,X)) V21( bool the carrier of (r,X), bool the carrier of r) Element of bool [:(bool the carrier of (r,X)),(bool the carrier of r):]
[:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
pr1 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of r -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of r) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of r:]
[:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty set
.: (pr1 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of r -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of r) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):]
bool [: the carrier of r, the carrier of X:] is non empty set
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
(r,X) is non empty Relation-like bool the carrier of (r,X) -defined bool the carrier of X -valued Function-like V20( bool the carrier of (r,X)) V21( bool the carrier of (r,X), bool the carrier of X) Element of bool [:(bool the carrier of (r,X)),(bool the carrier of X):]
[:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty set
pr2 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of X -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of X:]
[:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty set
.: (pr2 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of X -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of X) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):]
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty set
D is Element of bool the carrier of (r,X)
CH1 is Element of bool (bool the carrier of (r,X))
(r,X) .: CH1 is Element of bool (bool the carrier of r)
bool (bool the carrier of r) is non empty set
union ((r,X) .: CH1) is Element of bool the carrier of r
(r,X) .: CH1 is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
meet ((r,X) .: CH1) is Element of bool the carrier of X
(r,X,(union ((r,X) .: CH1)),(meet ((r,X) .: CH1))) is Relation-like Element of bool the carrier of (r,X)
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
bool the carrier of r is non empty Element of bool (bool the carrier of r)
bool the carrier of r is non empty set
bool (bool the carrier of r) is non empty set
X is non empty TopSpace-like TopStruct
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
bool the carrier of (r,X) is non empty set
bool (bool the carrier of (r,X)) is non empty set
bool the carrier of (r,X) is non empty Element of bool (bool the carrier of (r,X))
(r,X) is non empty Relation-like bool the carrier of (r,X) -defined bool the carrier of r -valued Function-like V20( bool the carrier of (r,X)) V21( bool the carrier of (r,X), bool the carrier of r) Element of bool [:(bool the carrier of (r,X)),(bool the carrier of r):]
[:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty set
the carrier of X is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
pr1 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of r -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of r) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of r:]
[:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty set
.: (pr1 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of r -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of r) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):]
bool [: the carrier of r, the carrier of X:] is non empty set
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty set
D is Element of bool (bool the carrier of (r,X))
(r,X) .: D is Element of bool (bool the carrier of r)
bool (bool the carrier of r) is non empty set
CH1 is set
dom (r,X) is non empty Element of bool (bool the carrier of (r,X))
bool (bool the carrier of (r,X)) is non empty set
II is set
(r,X) . II is set
THETA is Element of bool the carrier of (r,X)
(pr1 ( the carrier of r, the carrier of X)) .: THETA is Element of bool the carrier of r
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty TopSpace-like TopStruct
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
bool the carrier of (r,X) is non empty set
bool (bool the carrier of (r,X)) is non empty set
bool the carrier of (r,X) is non empty Element of bool (bool the carrier of (r,X))
the carrier of X is non empty set
bool the carrier 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
(r,X) is non empty Relation-like bool the carrier of (r,X) -defined bool the carrier of X -valued Function-like V20( bool the carrier of (r,X)) V21( bool the carrier of (r,X), bool the carrier of X) Element of bool [:(bool the carrier of (r,X)),(bool the carrier of X):]
[:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
pr2 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of X -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of X:]
[:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty set
.: (pr2 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of X -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of X) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):]
bool [: the carrier of r, the carrier of X:] is non empty set
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty set
D is Element of bool (bool the carrier of (r,X))
(r,X) .: D is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
CH1 is set
dom (r,X) is non empty Element of bool (bool the carrier of (r,X))
bool (bool the carrier of (r,X)) is non empty set
II is set
(r,X) . II is set
THETA is Element of bool the carrier of (r,X)
(pr2 ( the carrier of r, the carrier of X)) .: THETA is Element of bool the carrier of X
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
bool the carrier of r is non empty set
X is non empty TopSpace-like TopStruct
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
bool the carrier of (r,X) is non empty set
the carrier of X is non empty set
bool the carrier of X is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
pr1 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of r -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of r) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of r:]
[:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty set
pr2 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of X -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of X:]
[:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty set
D is Element of bool the carrier of (r,X)
(pr1 ( the carrier of r, the carrier of X)) .: D is Element of bool the carrier of r
(pr2 ( the carrier of r, the carrier of X)) .: D is Element of bool the carrier of X
.: (pr2 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of X -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of X) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):]
bool [: the carrier of r, the carrier of X:] is non empty set
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty set
bool (bool the carrier of (r,X)) is non empty set
THETA is Element of bool (bool the carrier of (r,X))
union THETA is Element of bool the carrier of (r,X)
bool (bool [: the carrier of r, the carrier of X:]) is non empty set
THETA9 is Element of bool the carrier of r
THETA99 is Element of bool the carrier of X
.: (pr1 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of r -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of r) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):]
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty set
bool (bool the carrier of r) is non empty set
THETA is Element of bool (bool [: the carrier of r, the carrier of X:])
(.: (pr1 ( the carrier of r, the carrier of X))) .: THETA is Element of bool (bool the carrier of r)
T is Element of bool (bool the carrier of r)
T is Element of bool (bool the carrier of r)
GG is Element of bool the carrier of r
U is Element of bool the carrier of r
V is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
(.: (pr1 ( the carrier of r, the carrier of X))) . V is Element of bool the carrier of r
dom (.: (pr1 ( the carrier of r, the carrier of X))) is non empty Element of bool (bool [: the carrier of r, the carrier of X:])
bool [: the carrier of r, the carrier of X:] is non empty Element of bool (bool [: the carrier of r, the carrier of X:])
(pr1 ( the carrier of r, the carrier of X)) .: V is Element of bool the carrier of r
H9 is Element of bool the carrier of r
H99 is Element of bool the carrier of X
(r,X,H9,H99) is Relation-like Element of bool the carrier of (r,X)
union ((.: (pr1 ( the carrier of r, the carrier of X))) .: THETA) is Element of bool the carrier of r
bool (bool the carrier of X) is non empty set
THETA is Element of bool (bool [: the carrier of r, the carrier of X:])
(.: (pr2 ( the carrier of r, the carrier of X))) .: THETA is Element of bool (bool the carrier of X)
W is Element of bool (bool the carrier of X)
W9 is Element of bool (bool the carrier of X)
T is Element of bool the carrier of X
T is Element of bool the carrier of X
GG is Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
(.: (pr2 ( the carrier of r, the carrier of X))) . GG is Element of bool the carrier of X
dom (.: (pr2 ( the carrier of r, the carrier of X))) is non empty Element of bool (bool [: the carrier of r, the carrier of X:])
bool [: the carrier of r, the carrier of X:] is non empty Element of bool (bool [: the carrier of r, the carrier of X:])
(pr2 ( the carrier of r, the carrier of X)) .: GG is Element of bool the carrier of X
U is Element of bool the carrier of r
V is Element of bool the carrier of X
(r,X,U,V) is Relation-like Element of bool the carrier of (r,X)
union ((.: (pr2 ( the carrier of r, the carrier of X))) .: THETA) is Element of bool the carrier of X
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
bool the carrier of r is non empty Element of bool (bool the carrier of r)
bool the carrier of r is non empty set
bool (bool the carrier of r) is non empty set
X is non empty TopSpace-like TopStruct
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
bool the carrier of (r,X) is non empty set
bool (bool the carrier of (r,X)) is non empty set
bool the carrier of (r,X) is non empty Element of bool (bool the carrier of (r,X))
(r,X) is non empty Relation-like bool the carrier of (r,X) -defined bool the carrier of r -valued Function-like V20( bool the carrier of (r,X)) V21( bool the carrier of (r,X), bool the carrier of r) Element of bool [:(bool the carrier of (r,X)),(bool the carrier of r):]
[:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty set
the carrier of X is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
pr1 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of r -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of r) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of r:]
[:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty set
.: (pr1 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of r -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of r) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):]
bool [: the carrier of r, the carrier of X:] is non empty set
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty set
bool the carrier 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
(r,X) is non empty Relation-like bool the carrier of (r,X) -defined bool the carrier of X -valued Function-like V20( bool the carrier of (r,X)) V21( bool the carrier of (r,X), bool the carrier of X) Element of bool [:(bool the carrier of (r,X)),(bool the carrier of X):]
[:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty set
pr2 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of X -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of X:]
[:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty set
.: (pr2 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of X -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of X) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):]
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty set
D is Element of bool (bool the carrier of (r,X))
(r,X) .: D is Element of bool (bool the carrier of r)
bool (bool the carrier of r) is non empty set
(r,X) .: D is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
II is Element of bool (bool the carrier of X)
THETA is Element of bool the carrier of X
THETA is Element of bool the carrier of (r,X)
(pr2 ( the carrier of r, the carrier of X)) .: THETA is Element of bool the carrier of X
CH1 is Element of bool (bool the carrier of r)
THETA is Element of bool the carrier of r
THETA is Element of bool the carrier of (r,X)
(pr1 ( the carrier of r, the carrier of X)) .: THETA is Element of bool the carrier of r
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
bool the carrier of r is non empty Element of bool (bool the carrier of r)
bool the carrier of r is non empty set
bool (bool the carrier of r) is non empty set
X is non empty TopSpace-like TopStruct
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
bool the carrier of (r,X) is non empty set
bool (bool the carrier of (r,X)) is non empty set
bool the carrier of (r,X) is non empty Element of bool (bool the carrier of (r,X))
(r,X) is non empty Relation-like bool the carrier of (r,X) -defined bool the carrier of r -valued Function-like V20( bool the carrier of (r,X)) V21( bool the carrier of (r,X), bool the carrier of r) Element of bool [:(bool the carrier of (r,X)),(bool the carrier of r):]
[:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty set
the carrier of X is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
pr1 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of r -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of r) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of r:]
[:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty set
.: (pr1 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of r -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of r) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):]
bool [: the carrier of r, the carrier of X:] is non empty set
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty set
bool the carrier 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
(r,X) is non empty Relation-like bool the carrier of (r,X) -defined bool the carrier of X -valued Function-like V20( bool the carrier of (r,X)) V21( bool the carrier of (r,X), bool the carrier of X) Element of bool [:(bool the carrier of (r,X)),(bool the carrier of X):]
[:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty set
pr2 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of X -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of X:]
[:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty set
.: (pr2 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of X -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of X) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):]
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty set
D is Element of bool (bool the carrier of (r,X))
(r,X) .: D is Element of bool (bool the carrier of r)
bool (bool the carrier of r) is non empty set
(r,X) .: D is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
dom (r,X) is non empty Element of bool (bool the carrier of (r,X))
bool (bool the carrier of (r,X)) is non empty set
dom (r,X) is non empty Element of bool (bool the carrier of (r,X))
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
bool the carrier of r is non empty set
bool the carrier of r is non empty Element of bool (bool the carrier of r)
bool (bool the carrier of r) is non empty set
X is non empty TopSpace-like TopStruct
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
bool the carrier of (r,X) is non empty set
bool (bool the carrier of (r,X)) is non empty set
the carrier of X is non empty set
bool the carrier of X is non empty set
bool the carrier of (r,X) is non empty Element of bool (bool the carrier of (r,X))
(r,X) is non empty Relation-like bool the carrier of (r,X) -defined bool the carrier of r -valued Function-like V20( bool the carrier of (r,X)) V21( bool the carrier of (r,X), bool the carrier of r) Element of bool [:(bool the carrier of (r,X)),(bool the carrier of r):]
[:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty set
[: the carrier of r, the carrier of X:] is non empty Relation-like set
pr1 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of r -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of r) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of r:]
[:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of r:] is non empty set
.: (pr1 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of r -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of r) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):]
bool [: the carrier of r, the carrier of X:] is non empty set
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of r):] is non empty set
bool the carrier of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
(r,X) is non empty Relation-like bool the carrier of (r,X) -defined bool the carrier of X -valued Function-like V20( bool the carrier of (r,X)) V21( bool the carrier of (r,X), bool the carrier of X) Element of bool [:(bool the carrier of (r,X)),(bool the carrier of X):]
[:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool the carrier of (r,X)),(bool the carrier of X):] is non empty set
pr2 ( the carrier of r, the carrier of X) is non empty Relation-like [: the carrier of r, the carrier of X:] -defined the carrier of X -valued Function-like V20([: the carrier of r, the carrier of X:]) V21([: the carrier of r, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of r, the carrier of X:], the carrier of X:]
[:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of X:], the carrier of X:] is non empty set
.: (pr2 ( the carrier of r, the carrier of X)) is non empty Relation-like bool [: the carrier of r, the carrier of X:] -defined bool the carrier of X -valued Function-like V20( bool [: the carrier of r, the carrier of X:]) V21( bool [: the carrier of r, the carrier of X:], bool the carrier of X) Element of bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):]
[:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool [: the carrier of r, the carrier of X:]),(bool the carrier of X):] is non empty set
D is Element of bool (bool the carrier of (r,X))
(r,X) .: D is Element of bool (bool the carrier of r)
bool (bool the carrier of r) is non empty set
(r,X) .: D is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
CH1 is Element of bool the carrier of r
II is Element of bool the carrier of X
(r,X,CH1,II) is Relation-like Element of bool the carrier of (r,X)
dom (.: (pr2 ( the carrier of r, the carrier of X))) is non empty Element of bool (bool [: the carrier of r, the carrier of X:])
bool (bool [: the carrier of r, the carrier of X:]) is non empty set
dom (pr2 ( the carrier of r, the carrier of X)) is non empty Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
bool (dom (pr2 ( the carrier of r, the carrier of X))) is non empty Element of bool (bool (dom (pr2 ( the carrier of r, the carrier of X))))
bool (dom (pr2 ( the carrier of r, the carrier of X))) is non empty set
bool (bool (dom (pr2 ( the carrier of r, the carrier of X)))) is non empty set
bool [: the carrier of r, the carrier of X:] is non empty Element of bool (bool [: the carrier of r, the carrier of X:])
union D is Element of bool the carrier of (r,X)
THETA is Element of the carrier of X
THETA is set
union ((r,X) .: D) is set
THETA9 is Element of the carrier of r
(r,X,THETA9,THETA) is non empty V7() Element of the carrier of (r,X)
{THETA9,THETA} is non empty finite set
{THETA9} is non empty trivial finite set
{{THETA9,THETA},{THETA9}} is non empty finite V28() set
THETA99 is set
dom (pr1 ( the carrier of r, the carrier of X)) is non empty Relation-like the carrier of r -defined the carrier of X -valued Element of bool [: the carrier of r, the carrier of X:]
dom (.: (pr1 ( the carrier of r, the carrier of X))) is non empty Element of bool (bool [: the carrier of r, the carrier of X:])
bool (dom (pr1 ( the carrier of r, the carrier of X))) is non empty Element of bool (bool (dom (pr1 ( the carrier of r, the carrier of X))))
bool (dom (pr1 ( the carrier of r, the carrier of X))) is non empty set
bool (bool (dom (pr1 ( the carrier of r, the carrier of X)))) is non empty set
(pr1 ( the carrier of r, the carrier of X)) . (THETA9,THETA) is Element of the carrier of r
[THETA9,THETA] is non empty V7() set
(pr1 ( the carrier of r, the carrier of X)) . [THETA9,THETA] is set
(pr1 ( the carrier of r, the carrier of X)) .: THETA99 is Element of bool the carrier of r
(.: (pr1 ( the carrier of r, the carrier of X))) . THETA99 is set
union ((r,X) .: D) is Element of bool the carrier of r
THETA is Element of the carrier of r
THETA is set
union ((r,X) .: D) is set
THETA9 is Element of the carrier of X
(r,X,THETA,THETA9) is non empty V7() Element of the carrier of (r,X)
{THETA,THETA9} is non empty finite set
{THETA} is non empty trivial finite set
{{THETA,THETA9},{THETA}} is non empty finite V28() set
THETA99 is set
(pr2 ( the carrier of r, the carrier of X)) . (THETA,THETA9) is Element of the carrier of X
[THETA,THETA9] is non empty V7() set
(pr2 ( the carrier of r, the carrier of X)) . [THETA,THETA9] is set
(pr2 ( the carrier of r, the carrier of X)) .: THETA99 is Element of bool the carrier of X
(.: (pr2 ( the carrier of r, the carrier of X))) . THETA99 is set
union ((r,X) .: D) is Element of bool the carrier of X

the carrier of r is set
bool the carrier of r is non empty set
bool (bool the carrier of r) is non empty set
D is Element of bool (bool the carrier of r)
CH1 is Element of bool the carrier of r
{ b1 where b1 is Element of bool the carrier of r : S1[b1] } is set
{ b1 where b1 is Element of bool the carrier of r : ( b1 in D & not b1 /\ CH1 = {} ) } is set
II is Element of bool (bool the carrier of r)
THETA is Element of bool (bool the carrier of r)
THETA is set
THETA9 is Element of bool the carrier of r
THETA9 /\ CH1 is Element of bool the carrier of r
union D is Element of bool the carrier of r
THETA is set
union THETA is set
THETA9 is set
THETA99 is Element of bool the carrier of r
THETA99 /\ CH1 is Element of bool the carrier of r
union THETA is Element of bool the carrier of r
THETA is set
THETA /\ CH1 is Element of bool the carrier of r
THETA9 is Element of bool the carrier of r
THETA9 /\ CH1 is Element of bool the carrier of r
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
bool the carrier of r is non empty set
bool (bool the carrier of r) is non empty set
bool the carrier of r is non empty Element of bool (bool the carrier of r)
X is non empty TopSpace-like TopStruct
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
bool the carrier of (r,X) is non empty set
bool (bool the carrier of (r,X)) is non empty set
bool the carrier of (r,X) is non empty Element of bool (bool the carrier of (r,X))
(r,X) is non empty Relation-like bool the carrier of (r,X) -defined bool the carrier of r -valued Function-like V20( bool the carrier of (r,X)) V21( bool the carrier of (r,X), bool the carrier of r) Element of bool [:(bool the carrier of (r,X)),(bool the carrier of r):]
[:(bool the carrier of (r,X)),(bool the carrier of r):] is non empty