:: 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
{} 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
the 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 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
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
[:[:1,1:],REAL:] is Relation-like set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is Relation-like set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] 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
[:[:2,2:],REAL:] is Relation-like set
bool [:[:2,2:],REAL:] is non empty set
union {} is finite set
RealSpace is non empty strict Reflexive discerning V112() triangle Discerning MetrStruct
real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like V21([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
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
r is TopSpace-like TopStruct
the carrier of r is set
X is TopSpace-like TopStruct
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
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( b₁ in the topology of r & b₂ 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 b₁) where b₁ is Element of bool (bool [: the carrier of r, the carrier of X:]) : b₁ c= { [:b₁,b₂:] where b₂ is Element of bool the carrier of r, b₃ is Element of bool the carrier of X : ( b₁ in the topology of r & b₂ 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 #)
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( b₁ in the topology of r & b₂ in the topology of X & ex b₃ being set st
( b₃ in THETA9 & [:b₁,b₂:] c= b₃ ) ) } 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 #)
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( b₁ in the topology of r & b₂ in the topology of X & [:b₁,b₂:] 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 b₁) where b₁ is Element of bool (bool the carrier of THETA) : b₁ c= { [:b₁,b₂:] where b₂ is Element of bool the carrier of r, b₃ is Element of bool the carrier of X : ( b₁ in the topology of r & b₂ in the topology of X ) } } is set
D is strict TopSpace-like TopStruct
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 b₁) where b₁ is Element of bool (bool the carrier of D) : b₁ c= { [:b₁,b₂:] where b₂ is Element of bool the carrier of r, b₃ is Element of bool the carrier of X : ( b₁ in the topology of r & b₂ in the topology of X ) } } is set
CH1 is strict TopSpace-like TopStruct
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 b₁) where b₁ is Element of bool (bool the carrier of CH1) : b₁ c= { [:b₁,b₂:] where b₂ is Element of bool the carrier of r, b₃ is Element of bool the carrier of X : ( b₁ in the topology of r & b₂ in the topology of X ) } } is set
r is TopSpace-like TopStruct
X is empty trivial finite {} -element TopSpace-like T_0 TopStruct
(r,X) is strict TopSpace-like TopStruct
the carrier of (r,X) is set
the carrier of r is set
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
[: 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 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
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 is TopSpace-like TopStruct
X is TopSpace-like TopStruct
(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
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( b₁ in the topology of r & b₂ in the topology of X ) } is set
{ (union b₁) where b₁ is Element of bool (bool the carrier of (r,X)) : b₁ c= { [:b₁,b₂:] where b₂ is Element of bool the carrier of r, b₃ is Element of bool the carrier of X : ( b₁ in the topology of r & b₂ 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
r is TopSpace-like TopStruct
the carrier of r is set
bool the carrier of r is non empty set
X is TopSpace-like TopStruct
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
r is TopSpace-like TopStruct
the carrier of r is set
bool the carrier of r is non empty set
X is TopSpace-like TopStruct
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)
r is TopSpace-like TopStruct
the carrier of r is set
bool the carrier of r is non empty set
X is TopSpace-like TopStruct
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 is TopSpace-like TopStruct
X is TopSpace-like TopStruct
(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,b₁,b₂) where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( (r,X,b₁,b₂) c= D & b₁ is open & b₂ 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 is TopSpace-like TopStruct
X is TopSpace-like TopStruct
(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,b₁,b₂) where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( (r,X,b₁,b₂) c= D & b₁ is open & b₂ 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 is TopSpace-like TopStruct
X is TopSpace-like TopStruct
(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,b₁,b₂) where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( (r,X,b₁,b₂) c= D & b₁ is open & b₂ is open ) } is set
(r,X,CH1) is open Element of bool (bool the carrier of (r,X))
{ (r,X,b₁,b₂) where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( (r,X,b₁,b₂) c= CH1 & b₁ is open & b₂ 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 is TopSpace-like TopStruct
X is TopSpace-like TopStruct
(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,b₁,b₂) where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( (r,X,b₁,b₂) c= D & b₁ is open & b₂ 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 is TopSpace-like TopStruct
X is TopSpace-like TopStruct
(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,b₁,b₂) where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( (r,X,b₁,b₂) c= D & b₁ is open & b₂ 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 is TopSpace-like TopStruct
X is TopSpace-like TopStruct
(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,b₁,b₂) where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( (r,X,b₁,b₂) c= D & b₁ is open & b₂ 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,b₁,b₂) where b₁ is Element of bool the carrier of r, b₂ is Element of bool the carrier of X : ( (r,X,b₁,b₂) c= Int D & b₁ is open & b₂ 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
r is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of bool the carrier of r : S₁[b₁] } is set
{ b₁ where b₁ is Element of bool the carrier of r : ( b₁ in D & not b₁ /\ 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