:: 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 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)
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
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
II is Relation-like Function-like set
dom II is set
II .: D is set
THETA is set
THETA is set
II . THETA is set
THETA is Element of bool (bool the carrier of (r,X))
(r,X) .: THETA is Element of bool (bool the carrier of r)
THETA is set
II . THETA is set
(r,X) . (II . THETA) is set
THETA9 is set
(r,X) . THETA9 is set
THETA99 is set
II . THETA99 is 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
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
(r,X,D,CH1) is Relation-like Element of bool the carrier of (r,X)
(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 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
(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) is non empty Element of bool (bool the carrier of (r,X))
bool (bool the carrier of (r,X)) 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
[: 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
(r,X) . (r,X,D,CH1) is Element of bool the carrier of r
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
(r,X) . (r,X,D,CH1) is 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
bool the carrier of X is non empty set
(X,r) is non empty strict TopSpace-like TopStruct
D is Element of the carrier of r
{D} is non empty trivial finite compact Element of bool the carrier of r
bool the carrier of r is non empty set
CH1 is Element of bool the carrier of X
(X,r,CH1,{D}) is Relation-like Element of bool the carrier of (X,r)
the carrier of (X,r) is non empty set
bool the carrier of (X,r) is non empty set
II is a_neighborhood of (X,r,CH1,{D})
[: the carrier of X, the carrier of r:] is non empty Relation-like set
{} X is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V28() V29() V30() V31() V32() V33() V34() V35() open closed boundary nowhere_dense Element of bool the carrier of X
Int II is open Element of bool the carrier of (X,r)
(X,r,II) is open Element of bool (bool the carrier of (X,r))
bool (bool the carrier of (X,r)) is non empty set
{ (X,r,b₁,b₂) where b₁ is Element of bool the carrier of X, b₂ is Element of bool the carrier of r : ( (X,r,b₁,b₂) c= II & b₁ is open & b₂ is open ) } is set
union (X,r,II) is Element of bool the carrier of (X,r)
THETA is Element of bool (bool the carrier of (X,r))
bool (bool the carrier of X) is non empty set
bool the carrier of (X,r) is non empty Element of bool (bool the carrier of (X,r))
bool the carrier of X is non empty Element of bool (bool the carrier of X)
(X,r) is non empty Relation-like bool the carrier of (X,r) -defined bool the carrier of X -valued Function-like V20( bool the carrier of (X,r)) V21( bool the carrier of (X,r), bool the carrier of X) Element of bool [:(bool the carrier of (X,r)),(bool the carrier of X):]
[:(bool the carrier of (X,r)),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool the carrier of (X,r)),(bool the carrier of X):] is non empty set
pr1 ( the carrier of X, the carrier of r) is non empty Relation-like [: the carrier of X, the carrier of r:] -defined the carrier of X -valued Function-like V20([: the carrier of X, the carrier of r:]) V21([: the carrier of X, the carrier of r:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of r:], the carrier of X:]
[:[: the carrier of X, the carrier of r:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of r:], the carrier of X:] is non empty set
.: (pr1 ( the carrier of X, the carrier of r)) is non empty Relation-like bool [: the carrier of X, the carrier of r:] -defined bool the carrier of X -valued Function-like V20( bool [: the carrier of X, the carrier of r:]) V21( bool [: the carrier of X, the carrier of r:], bool the carrier of X) Element of bool [:(bool [: the carrier of X, the carrier of r:]),(bool the carrier of X):]
bool [: the carrier of X, the carrier of r:] is non empty set
[:(bool [: the carrier of X, the carrier of r:]),(bool the carrier of X):] is non empty Relation-like set
bool [:(bool [: the carrier of X, the carrier of r:]),(bool the carrier of X):] is non empty set
(X,r) .: THETA is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
THETA is Element of bool (bool the carrier of X)
THETA9 is Element of bool (bool the carrier of X)
THETA99 is Element of bool (bool the carrier of (X,r))
(X,r) .: THETA99 is Element of bool (bool 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
union THETA99 is set
union THETA9 is Element of bool the carrier of X
[W9,T] `2 is set
[W9,T] `1 is set
[([W9,T] `1),D] is non empty V7() set
{([W9,T] `1),D} is non empty finite set
{([W9,T] `1)} is non empty trivial finite set
{{([W9,T] `1),D},{([W9,T] `1)}} is non empty finite V28() set
T is set
GG is Element of bool the carrier of (X,r)
(X,r) . GG is Element of bool the carrier of X
U is Element of bool the carrier of X
V is Element of bool the carrier of r
(X,r,U,V) is Relation-like Element of bool the carrier of (X,r)
H9 is set
H9 `2 is set
union THETA99 is Element of bool the carrier of (X,r)
W is Element of bool (bool the carrier of X)
union W is Element of bool the carrier of X
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,r) is non empty Relation-like bool the carrier of (X,r) -defined bool the carrier of r -valued Function-like V20( bool the carrier of (X,r)) V21( bool the carrier of (X,r), bool the carrier of r) Element of bool [:(bool the carrier of (X,r)),(bool the carrier of r):]
[:(bool the carrier of (X,r)),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool the carrier of (X,r)),(bool the carrier of r):] is non empty set
pr2 ( the carrier of X, the carrier of r) is non empty Relation-like [: the carrier of X, the carrier of r:] -defined the carrier of r -valued Function-like V20([: the carrier of X, the carrier of r:]) V21([: the carrier of X, the carrier of r:], the carrier of r) Element of bool [:[: the carrier of X, the carrier of r:], the carrier of r:]
[:[: the carrier of X, the carrier of r:], the carrier of r:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of r:], the carrier of r:] is non empty set
.: (pr2 ( the carrier of X, the carrier of r)) is non empty Relation-like bool [: the carrier of X, the carrier of r:] -defined bool the carrier of r -valued Function-like V20( bool [: the carrier of X, the carrier of r:]) V21( bool [: the carrier of X, the carrier of r:], bool the carrier of r) Element of bool [:(bool [: the carrier of X, the carrier of r:]),(bool the carrier of r):]
[:(bool [: the carrier of X, the carrier of r:]),(bool the carrier of r):] is non empty Relation-like set
bool [:(bool [: the carrier of X, the carrier of r:]),(bool the carrier of r):] is non empty set
(X,r) .: THETA99 is Element of bool (bool the carrier of r)
bool (bool the carrier of r) is non empty set
T is set
W9 is Element of bool (bool the carrier of r)
T is Element of bool the carrier of (X,r)
(pr2 ( the carrier of X, the carrier of r)) .: T is Element of bool the carrier of r
T /\ (X,r,CH1,{D}) is Relation-like Element of bool the carrier of (X,r)
GG is Element of the carrier of (X,r)
GG `1 is set
(pr2 ( the carrier of X, the carrier of r)) . ((GG `1),D) is set
[(GG `1),D] is non empty V7() set
{(GG `1),D} is non empty finite set
{(GG `1)} is non empty trivial finite set
{{(GG `1),D},{(GG `1)}} is non empty finite V28() set
(pr2 ( the carrier of X, the carrier of r)) . [(GG `1),D] is set
GG `2 is set
union THETA99 is Element of bool the carrier of (X,r)
meet W9 is Element of bool the carrier of r
Int (meet W9) is open Element of bool the carrier of r
Int (union W) is open Element of bool the carrier of X
T is a_neighborhood of CH1
T is a_neighborhood of D
V is set
H9 is Element of bool the carrier of X
H99 is Element of bool the carrier of r
(X,r,H9,H99) is Relation-like Element of bool the carrier of (X,r)
GG is a_neighborhood of CH1
U is a_neighborhood of D
(X,r,CH1,D,GG,U) is Relation-like a_neighborhood of (X,r,CH1,{D})
{} X is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V28() V29() V30() V31() V32() V33() V34() V35() open closed boundary nowhere_dense Element of bool the carrier of X
Int ({} X) is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V28() V29() V30() V31() V32() V33() V34() V35() open closed boundary nowhere_dense Element of bool the carrier of X
the a_neighborhood of D is a_neighborhood of D
THETA is a_neighborhood of CH1
THETA9 is a_neighborhood of CH1
THETA99 is a_neighborhood of D
(X,r,CH1,D,THETA9,THETA99) is Relation-like a_neighborhood of (X,r,CH1,{D})
{} X is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V28() V29() V30() V31() V32() V33() V34() V35() open closed boundary nowhere_dense Element of bool the carrier of X
THETA is a_neighborhood of CH1
THETA is a_neighborhood of D
(X,r,CH1,D,THETA,THETA) is Relation-like a_neighborhood of (X,r,CH1,{D})
r is 1-sorted
the carrier of r is set
id the carrier of r is Relation-like the carrier of r -defined the carrier of r -valued Function-like one-to-one V20( the carrier of r) V21( the carrier of r, the carrier of r) V22( the carrier of r) V23( the carrier of r, the carrier of r) V36() V38() V39() V43() Element of bool [: the carrier of r, the carrier of r:]
[: the carrier of r, the carrier of r:] is Relation-like set
bool [: the carrier of r, the carrier of r:] is non empty set
Class (id the carrier of r) is with_non-empty_elements a_partition of the carrier of r
r is non empty 1-sorted
(r) is non empty with_non-empty_elements a_partition of the carrier of r
the carrier of r is non empty set
id the carrier of r is non empty Relation-like the carrier of r -defined the carrier of r -valued Function-like one-to-one V20( the carrier of r) V21( the carrier of r, the carrier of r) V22( the carrier of r) V23( the carrier of r, the carrier of r) V36() V38() V39() V43() Element of bool [: the carrier of r, the carrier of r:]
[: the carrier of r, the carrier of r:] is non empty Relation-like set
bool [: the carrier of r, the carrier of r:] is non empty set
Class (id the carrier of r) is non empty with_non-empty_elements a_partition of 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
(r) is non empty with_non-empty_elements a_partition of the carrier of r
id the carrier of r is non empty Relation-like the carrier of r -defined the carrier of r -valued Function-like one-to-one V20( the carrier of r) V21( the carrier of r, the carrier of r) V22( the carrier of r) V23( the carrier of r, the carrier of r) V36() V38() V39() V43() Element of bool [: the carrier of r, the carrier of r:]
[: the carrier of r, the carrier of r:] is non empty Relation-like set
bool [: the carrier of r, the carrier of r:] is non empty set
Class (id the carrier of r) is non empty with_non-empty_elements a_partition of the carrier of r
X is Element of bool the carrier of r
D is set
Class ((id the carrier of r),D) is Element of bool the carrier of r
{D} is non empty trivial finite set
(id the carrier of r) .: {D} is finite set
CH1 is Element of the carrier of r
{CH1} is non empty trivial finite compact 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
(r) is non empty with_non-empty_elements a_partition of the carrier of r
id the carrier of r is non empty Relation-like the carrier of r -defined the carrier of r -valued Function-like one-to-one V20( the carrier of r) V21( the carrier of r, the carrier of r) V22( the carrier of r) V23( the carrier of r, the carrier of r) V36() V38() V39() V43() Element of bool [: the carrier of r, the carrier of r:]
[: the carrier of r, the carrier of r:] is non empty Relation-like set
bool [: the carrier of r, the carrier of r:] is non empty set
Class (id the carrier of r) is non empty with_non-empty_elements a_partition of the carrier of r
X is Element of bool the carrier of r
D is a_neighborhood of X
Int D is open Element of bool the carrier of r
CH1 is Element of bool the carrier of r
II is Element of the carrier of r
{II} is non empty trivial finite compact Element of bool the carrier of r
r is TopSpace-like TopStruct
the carrier of r is set
X is with_non-empty_elements a_partition of the carrier of r
bool X is non empty set
the topology 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
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : union b<sub>1</sub> in the topology of r } is set
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
CH1 is set
II is Element of bool X
union II is set
CH1 is Element of bool (bool X)
TopStruct(# X,CH1 #) is strict TopStruct
union X is Element of bool the carrier of r
the carrier of TopStruct(# X,CH1 #) is set
the topology of TopStruct(# X,CH1 #) is Element of bool (bool the carrier of TopStruct(# X,CH1 #))
bool the carrier of TopStruct(# X,CH1 #) is non empty set
bool (bool the carrier of TopStruct(# X,CH1 #)) is non empty set
THETA is Element of bool (bool the carrier of TopStruct(# X,CH1 #))
union THETA is Element of bool the carrier of TopStruct(# X,CH1 #)
{ (union b<sub>1</sub>) where b<sub>1</sub> is Element of bool the carrier of TopStruct(# X,CH1 #) : b<sub>1</sub> in THETA } is set
bool the carrier of r is non empty Element of bool (bool the carrier of r)
THETA is set
THETA9 is Element of bool the carrier of TopStruct(# X,CH1 #)
union THETA9 is set
THETA99 is set
W is set
THETA is set
THETA9 is Element of bool the carrier of TopStruct(# X,CH1 #)
union THETA9 is set
THETA99 is Element of bool X
union THETA99 is set
union { (union b<sub>1</sub>) where b<sub>1</sub> is Element of bool the carrier of TopStruct(# X,CH1 #) : b<sub>1</sub> in THETA } is set
union (union THETA) is set
THETA is Element of bool the carrier of TopStruct(# X,CH1 #)
THETA is Element of bool the carrier of TopStruct(# X,CH1 #)
THETA /\ THETA is Element of bool the carrier of TopStruct(# X,CH1 #)
THETA9 is Element of bool X
union THETA9 is set
THETA99 is Element of bool X
union THETA99 is set
THETA99 /\ THETA9 is Element of bool X
union (THETA99 /\ THETA9) is set
(union THETA99) /\ (union THETA9) is set
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
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
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
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty with_non-empty_elements a_partition of the carrier of r
(r,X) is strict TopSpace-like TopStruct
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
the topology 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 with_non-empty_elements a_partition of the carrier of r
bool X is non empty set
(r,X) is non empty strict TopSpace-like TopStruct
the topology of (r,X) is non empty Element of bool (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
bool (bool the carrier of (r,X)) is non empty set
D is Element of bool X
union D is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool X : union b<sub>1</sub> in the topology of r } is set
CH1 is Element of bool X
union CH1 is set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty with_non-empty_elements a_partition of the carrier of r
proj X is non empty Relation-like the carrier of r -defined X -valued Function-like V20( the carrier of r) V21( the carrier of r,X) Element of bool [: the carrier of r,X:]
[: the carrier of r,X:] is non empty Relation-like set
bool [: the carrier of r,X:] is non empty set
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
[: the carrier of r, the carrier of (r,X):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,X):] is non empty set
D is non empty Relation-like the carrier of r -defined the carrier of (r,X) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,X)) Element of bool [: the carrier of r, the carrier of (r,X):]
CH1 is Element of the carrier of r
D . CH1 is Element of the carrier of (r,X)
II is a_neighborhood of D . CH1
bool the carrier of r is non empty set
Int II is open Element of bool the carrier of (r,X)
bool the carrier of (r,X) is non empty set
union (Int II) is set
D " (Int II) is Element of bool the carrier of r
the topology of (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
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
THETA is Element of bool the carrier of r
Int THETA is open Element of bool the carrier of r
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 (r,X)
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
D is Element of the carrier of r
X is non empty with_non-empty_elements a_partition of the carrier of r
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
(r,X) is non empty Relation-like the carrier of r -defined the carrier of (r,X) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,X)) continuous Element of bool [: the carrier of r, the carrier of (r,X):]
[: the carrier of r, the carrier of (r,X):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,X):] is non empty set
proj X is non empty Relation-like the carrier of r -defined X -valued Function-like V20( the carrier of r) V21( the carrier of r,X) Element of bool [: the carrier of r,X:]
[: the carrier of r,X:] is non empty Relation-like set
bool [: the carrier of r,X:] is non empty set
(r,X) . D is Element of the carrier of (r,X)
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty with_non-empty_elements a_partition of the carrier of r
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
(r,X) is non empty Relation-like the carrier of r -defined the carrier of (r,X) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,X)) continuous Element of bool [: the carrier of r, the carrier of (r,X):]
[: the carrier of r, the carrier of (r,X):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,X):] is non empty set
proj X is non empty Relation-like the carrier of r -defined X -valued Function-like V20( the carrier of r) V21( the carrier of r,X) Element of bool [: the carrier of r,X:]
[: the carrier of r,X:] is non empty Relation-like set
bool [: the carrier of r,X:] is non empty set
D is Element of the carrier of (r,X)
bool the carrier of r is non empty set
CH1 is Element of X
II is Element of the carrier of r
(proj X) . II is Element of X
(r,X) . II is Element of the carrier of (r,X)
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty with_non-empty_elements a_partition of the carrier of r
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
(r,X) is non empty Relation-like the carrier of r -defined the carrier of (r,X) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,X)) continuous Element of bool [: the carrier of r, the carrier of (r,X):]
[: the carrier of r, the carrier of (r,X):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,X):] is non empty set
proj X is non empty Relation-like the carrier of r -defined X -valued Function-like V20( the carrier of r) V21( the carrier of r,X) Element of bool [: the carrier of r,X:]
[: the carrier of r,X:] is non empty Relation-like set
bool [: the carrier of r,X:] is non empty set
rng (r,X) is non empty Element of bool the carrier of (r,X)
bool the carrier of (r,X) is non empty set
D is set
CH1 is Element of the carrier of r
(r,X) . CH1 is Element of the carrier of (r,X)
r is non empty TopSpace-like TopStruct
X is non empty TopSpace-like SubSpace of r
the carrier of X is non empty set
D is non empty with_non-empty_elements a_partition of the carrier of X
the carrier of r is non empty set
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
D \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } 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
II is 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
THETA is Element of the carrier of r
{THETA} is non empty trivial finite compact Element of bool the carrier of r
II is Element of bool (bool the carrier of r)
THETA is set
the carrier of r \ the carrier of X is Element of bool the carrier of r
{THETA} is non empty trivial finite set
THETA is set
THETA9 is Element of the carrier of r
{THETA9} is non empty trivial finite compact Element of bool the carrier of r
union { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
union II is Element of bool the carrier of r
union D is Element of bool the carrier of X
bool the carrier of X is non empty set
(union D) \/ (union { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } ) is set
the carrier of X \/ ( the carrier of r \ the carrier of X) is non empty set
THETA is Element of bool the carrier of r
THETA is Element of the carrier of r
{THETA} is non empty trivial finite compact Element of bool the carrier of r
THETA is Element of bool the carrier of r
THETA9 is Element of the carrier of r
{THETA9} is non empty trivial finite compact Element of bool the carrier of r
THETA9 is Element of the carrier of r
{THETA9} is non empty trivial finite compact Element of bool the carrier of r
THETA9 is Element of the carrier of r
{THETA9} is non empty trivial finite compact Element of bool the carrier of r
THETA99 is Element of the carrier of r
{THETA99} is non empty trivial finite compact 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 non empty TopSpace-like SubSpace of r
the carrier of X is non empty set
[#] 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
D is non empty with_non-empty_elements a_partition of the carrier of X
(r,X,D) is non empty with_non-empty_elements a_partition of the carrier of r
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
D \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is non empty set
CH1 is Element of bool the carrier of r
II is Element of the carrier of r
{II} is non empty trivial finite compact Element of bool the carrier of r
THETA is Element of the carrier of r
{THETA} is non empty trivial finite compact Element of bool the carrier of r
II is Element of the carrier of r
{II} is non empty trivial finite compact 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 SubSpace of r
the carrier of X is non empty set
D is non empty with_non-empty_elements a_partition of the carrier of X
(r,X,D) is non empty with_non-empty_elements a_partition of the carrier of r
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
D \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is non empty set
CH1 is Element of the carrier of r
{CH1} is non empty trivial finite compact Element of bool the carrier of r
bool the carrier of r is non empty set
union (r,X,D) is Element of bool the carrier of r
II is set
THETA is Element of the carrier of r
{THETA} is non empty trivial finite compact 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 SubSpace of r
the carrier of X is non empty set
D is non empty with_non-empty_elements a_partition of the carrier of X
(r,X,D) is non empty with_non-empty_elements a_partition of the carrier of r
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
D \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is non empty set
(r,(r,X,D)) is non empty strict TopSpace-like TopStruct
the carrier of (r,(r,X,D)) is non empty set
(r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of r, the carrier of (r,(r,X,D)):]
[: the carrier of r, the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,(r,X,D)):] is non empty set
proj (r,X,D) is non empty Relation-like the carrier of r -defined (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r,(r,X,D)) Element of bool [: the carrier of r,(r,X,D):]
[: the carrier of r,(r,X,D):] is non empty Relation-like set
bool [: the carrier of r,(r,X,D):] is non empty set
(X,D) is non empty Relation-like the carrier of X -defined the carrier of (X,D) -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of (X,D)) continuous Element of bool [: the carrier of X, the carrier of (X,D):]
(X,D) is non empty strict TopSpace-like TopStruct
the carrier of (X,D) is non empty set
[: the carrier of X, the carrier of (X,D):] is non empty Relation-like set
bool [: the carrier of X, the carrier of (X,D):] is non empty set
proj D is non empty Relation-like the carrier of X -defined D -valued Function-like V20( the carrier of X) V21( the carrier of X,D) Element of bool [: the carrier of X,D:]
[: the carrier of X,D:] is non empty Relation-like set
bool [: the carrier of X,D:] is non empty set
CH1 is Element of the carrier of r
(r,(r,X,D)) . CH1 is Element of the carrier of (r,(r,X,D))
(X,D) . CH1 is set
II is Element of the carrier of X
(proj D) . II is Element of D
bool the carrier of r is non empty set
THETA is Element of (r,X,D)
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty TopSpace-like SubSpace of r
the carrier of X is non empty set
D is non empty with_non-empty_elements a_partition of the carrier of X
(r,X,D) is non empty with_non-empty_elements a_partition of the carrier of r
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
D \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is non empty set
(r,(r,X,D)) is non empty strict TopSpace-like TopStruct
the carrier of (r,(r,X,D)) is non empty set
(r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of r, the carrier of (r,(r,X,D)):]
[: the carrier of r, the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,(r,X,D)):] is non empty set
proj (r,X,D) is non empty Relation-like the carrier of r -defined (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r,(r,X,D)) Element of bool [: the carrier of r,(r,X,D):]
[: the carrier of r,(r,X,D):] is non empty Relation-like set
bool [: the carrier of r,(r,X,D):] is non empty set
CH1 is Element of the carrier of r
(r,(r,X,D)) . CH1 is Element of the carrier of (r,(r,X,D))
{CH1} is non empty trivial finite compact 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 SubSpace of r
the carrier of X is non empty set
D is non empty with_non-empty_elements a_partition of the carrier of X
(r,X,D) is non empty with_non-empty_elements a_partition of the carrier of r
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
D \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is non empty set
(r,(r,X,D)) is non empty strict TopSpace-like TopStruct
the carrier of (r,(r,X,D)) is non empty set
(r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of r, the carrier of (r,(r,X,D)):]
[: the carrier of r, the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,(r,X,D)):] is non empty set
proj (r,X,D) is non empty Relation-like the carrier of r -defined (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r,(r,X,D)) Element of bool [: the carrier of r,(r,X,D):]
[: the carrier of r,(r,X,D):] is non empty Relation-like set
bool [: the carrier of r,(r,X,D):] is non empty set
CH1 is Element of the carrier of r
(r,(r,X,D)) . CH1 is Element of the carrier of (r,(r,X,D))
II is Element of the carrier of r
(r,(r,X,D)) . II is Element of the carrier of (r,(r,X,D))
{CH1} is non empty trivial finite compact 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 SubSpace of r
the carrier of X is non empty set
D is non empty with_non-empty_elements a_partition of the carrier of X
(r,X,D) is non empty with_non-empty_elements a_partition of the carrier of r
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
D \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is non empty set
(r,(r,X,D)) is non empty strict TopSpace-like TopStruct
the carrier of (r,(r,X,D)) is non empty set
(r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of r, the carrier of (r,(r,X,D)):]
[: the carrier of r, the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,(r,X,D)):] is non empty set
proj (r,X,D) is non empty Relation-like the carrier of r -defined (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r,(r,X,D)) Element of bool [: the carrier of r,(r,X,D):]
[: the carrier of r,(r,X,D):] is non empty Relation-like set
bool [: the carrier of r,(r,X,D):] is non empty set
(X,D) is non empty strict TopSpace-like TopStruct
the carrier of (X,D) is non empty set
CH1 is Element of the carrier of r
(r,(r,X,D)) . CH1 is Element of the carrier of (r,(r,X,D))
r is non empty TopSpace-like TopStruct
X is non empty TopSpace-like SubSpace of r
the carrier of X is non empty set
D is non empty with_non-empty_elements a_partition of the carrier of X
(r,X,D) is non empty with_non-empty_elements a_partition of the carrier of r
the carrier of r is non empty set
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
D \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is non empty set
(r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of r, the carrier of (r,(r,X,D)):]
(r,(r,X,D)) is non empty strict TopSpace-like TopStruct
the carrier of (r,(r,X,D)) is non empty set
[: the carrier of r, the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,(r,X,D)):] is non empty set
proj (r,X,D) is non empty Relation-like the carrier of r -defined (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r,(r,X,D)) Element of bool [: the carrier of r,(r,X,D):]
[: the carrier of r,(r,X,D):] is non empty Relation-like set
bool [: the carrier of r,(r,X,D):] is non empty set
(X,D) is non empty strict TopSpace-like TopStruct
the carrier of (X,D) is non empty set
CH1 is set
(r,(r,X,D)) . CH1 is set
(X,D) is non empty Relation-like the carrier of X -defined the carrier of (X,D) -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of (X,D)) continuous Element of bool [: the carrier of X, the carrier of (X,D):]
[: the carrier of X, the carrier of (X,D):] is non empty Relation-like set
bool [: the carrier of X, the carrier of (X,D):] is non empty set
proj D is non empty Relation-like the carrier of X -defined D -valued Function-like V20( the carrier of X) V21( the carrier of X,D) Element of bool [: the carrier of X,D:]
[: the carrier of X,D:] is non empty Relation-like set
bool [: the carrier of X,D:] is non empty set
II is Element of the carrier of X
(X,D) . II is Element of the carrier of (X,D)
(r,(r,X,D)) . II is 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
(r) is non empty with_non-empty_elements a_partition of the carrier of r
id the carrier of r is non empty Relation-like the carrier of r -defined the carrier of r -valued Function-like one-to-one V20( the carrier of r) V21( the carrier of r, the carrier of r) V22( the carrier of r) V23( the carrier of r, the carrier of r) V36() V38() V39() V43() Element of bool [: the carrier of r, the carrier of r:]
[: the carrier of r, the carrier of r:] is non empty Relation-like set
bool [: the carrier of r, the carrier of r:] is non empty set
Class (id the carrier of r) is non empty with_non-empty_elements a_partition of the carrier of r
X is Element of bool the carrier of r
D is a_neighborhood of X
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty with_non-empty_elements (r)
(r,X) is non empty strict TopSpace-like TopStruct
the carrier of (r,X) is non empty set
(r,X) is non empty Relation-like the carrier of r -defined the carrier of (r,X) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,X)) continuous Element of bool [: the carrier of r, the carrier of (r,X):]
[: the carrier of r, the carrier of (r,X):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,X):] is non empty set
proj X is non empty Relation-like the carrier of r -defined X -valued Function-like V20( the carrier of r) V21( the carrier of r,X) Element of bool [: the carrier of r,X:]
[: the carrier of r,X:] is non empty Relation-like set
bool [: the carrier of r,X:] is non empty set
D is Element of the carrier of (r,X)
{D} is non empty trivial finite compact Element of bool the carrier of (r,X)
bool the carrier of (r,X) is non empty set
(r,X) " {D} is Element of bool the carrier of r
bool the carrier of r is non empty set
CH1 is a_neighborhood of (r,X) " {D}
(r,X) .: CH1 is Element of bool the carrier of (r,X)
II is Element of bool the carrier of r
(r,X) .: II is Element of bool the carrier of (r,X)
(r,X) .: ((r,X) " {D}) is Element of bool the carrier of (r,X)
union ((r,X) .: II) is set
(proj X) " ((r,X) .: II) is Element of bool the carrier of r
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 (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
rng (r,X) is non empty Element of bool the carrier of (r,X)
Int ((r,X) .: CH1) is open Element of bool the carrier of (r,X)
r is non empty TopSpace-like TopStruct
(r) is non empty with_non-empty_elements a_partition of the carrier of r
the carrier of r is non empty set
id the carrier of r is non empty Relation-like the carrier of r -defined the carrier of r -valued Function-like one-to-one V20( the carrier of r) V21( the carrier of r, the carrier of r) V22( the carrier of r) V23( the carrier of r, the carrier of r) V36() V38() V39() V43() Element of bool [: the carrier of r, the carrier of r:]
[: the carrier of r, the carrier of r:] is non empty Relation-like set
bool [: the carrier of r, the carrier of r:] is non empty set
Class (id the carrier of r) is non empty with_non-empty_elements a_partition of the carrier of r
bool the carrier of r is non empty set
X is Element of bool the carrier of r
D is a_neighborhood of X
r is TopSpace-like TopStruct
r is TopStruct
the carrier of r is set
the topology of r is 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
TopStruct(# the carrier of r, the topology of r #) is strict TopStruct
[#] TopStruct(# the carrier of r, the topology of r #) is non proper dense Element of bool the carrier of TopStruct(# the carrier of r, the topology of r #)
the carrier of TopStruct(# the carrier of r, the topology of r #) is set
bool the carrier of TopStruct(# the carrier of r, the topology of r #) is non empty set
[#] r is non proper dense Element of bool the carrier of r
the topology of TopStruct(# the carrier of r, the topology of r #) is Element of bool (bool the carrier of TopStruct(# the carrier of r, the topology of r #))
bool (bool the carrier of TopStruct(# the carrier of r, the topology of r #)) is non empty set
D is Element of bool the carrier of TopStruct(# the carrier of r, the topology of r #)
CH1 is Element of bool the carrier of r
II is Element of bool the carrier of r
II /\ ([#] TopStruct(# the carrier of r, the topology of r #)) is Element of bool the carrier of TopStruct(# the carrier of r, the topology of r #)
CH1 is Element of bool the carrier of r
CH1 /\ ([#] TopStruct(# the carrier of r, the topology of r #)) is Element of bool the carrier of TopStruct(# the carrier of r, the topology of r #)
r is TopSpace-like TopStruct
the carrier of r is set
the topology 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
TopStruct(# the carrier of r, the topology of r #) is strict TopSpace-like TopStruct
X is strict TopSpace-like SubSpace of r
D is Element of bool the carrier of r
the carrier of X is set
[#] r is non proper open closed dense Element of bool the carrier of r
r is non empty TopSpace-like TopStruct
[#] r is non empty non proper open closed dense non boundary Element of bool the carrier of r
the carrier of r is non empty set
bool the carrier of r is non empty set
r | ([#] r) is non empty strict TopSpace-like SubSpace of r
X is Element of bool the carrier of r
the carrier of (r | ([#] r)) is non empty set
[#] (r | ([#] r)) is non empty non proper open closed dense non boundary Element of bool the carrier of (r | ([#] r))
bool the carrier of (r | ([#] r)) is non empty set
r is non empty TopSpace-like TopStruct
X is non empty TopSpace-like (r) SubSpace of r
D is non empty with_non-empty_elements (X)
(r,X,D) is non empty with_non-empty_elements a_partition of the carrier of r
the carrier of r is non empty set
the carrier of X is non empty set
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
D \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is non empty set
bool the carrier of r is non empty set
CH1 is Element of bool the carrier of r
II is a_neighborhood of CH1
Int II is open Element of bool the carrier of r
bool the carrier of X is non empty set
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
(Int II) /\ ([#] X) is Element of bool the carrier of X
THETA is Element of bool the carrier of X
THETA is Element of bool the carrier of X
Int THETA is open Element of bool the carrier of X
THETA9 is Element of bool the carrier of X
THETA99 is Element of bool the carrier of r
THETA99 /\ ([#] X) is Element of bool the carrier of X
THETA99 /\ (Int II) is Element of bool the carrier of r
W is Element of bool the carrier of r
W9 is Element of bool the carrier of r
T is Element of the carrier of r
{T} is non empty trivial finite compact Element of bool the carrier of r
T is Element of the carrier of r
{T} is non empty trivial finite compact Element of bool the carrier of r
[#] 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
[#] r is non empty non proper open closed dense non boundary Element of bool the carrier of r
THETA is Element of bool the carrier of r
(Int II) \ THETA is Element of bool the carrier of r
THETA ` is Element of bool the carrier of r
the carrier of r \ THETA is set
(Int II) /\ (THETA `) is Element of bool the carrier of r
THETA is Element of bool the carrier of r
THETA9 is Element of the carrier of r
{THETA9} is non empty trivial finite compact Element of bool the carrier of r
THETA9 is Element of the carrier of r
{THETA9} is non empty trivial finite compact Element of bool the carrier of r
THETA99 is Element of bool the carrier of r
W is Element of the carrier of r
{W} is non empty trivial finite compact Element of bool the carrier of r
[#] 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
THETA is Element of bool the carrier of r
r is non empty TopSpace-like TopStruct
r is non empty TopSpace-like TopStruct
(r) is non empty with_non-empty_elements a_partition of the carrier of r
the carrier of r is non empty set
id the carrier of r is non empty Relation-like the carrier of r -defined the carrier of r -valued Function-like one-to-one V20( the carrier of r) V21( the carrier of r, the carrier of r) V22( the carrier of r) V23( the carrier of r, the carrier of r) V36() V38() V39() V43() Element of bool [: the carrier of r, the carrier of r:]
[: the carrier of r, the carrier of r:] is non empty Relation-like set
bool [: the carrier of r, the carrier of r:] is non empty set
Class (id the carrier of r) is non empty with_non-empty_elements a_partition of the carrier of r
X is non empty with_non-empty_elements (r)
bool the carrier of r is non empty set
D is Element of bool the carrier of r
CH1 is Element of the carrier of r
{CH1} is non empty trivial finite compact Element of bool the carrier of r
r is non empty TopSpace-like TopStruct
X is non empty TopSpace-like (r) SubSpace of r
D is non empty with_non-empty_elements (X) (X)
(r,X,D) is non empty with_non-empty_elements a_partition of the carrier of r
the carrier of r is non empty set
the carrier of X is non empty set
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
D \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is non empty set
(r,X,D) is non empty with_non-empty_elements (r)
bool the carrier of r is non empty set
CH1 is Element of bool the carrier of r
proj (r,X,D) is non empty Relation-like the carrier of r -defined (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r,(r,X,D)) Element of bool [: the carrier of r,(r,X,D):]
[: the carrier of r,(r,X,D):] is non empty Relation-like set
bool [: the carrier of r,(r,X,D):] is non empty set
II is Element of the carrier of r
(proj (r,X,D)) . II is Element of (r,X,D)
(r,(r,X,D)) is non empty strict TopSpace-like TopStruct
the carrier of (r,(r,X,D)) is non empty set
(r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of r, the carrier of (r,(r,X,D)):]
[: the carrier of r, the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,(r,X,D)):] is non empty set
(r,(r,X,D)) . II is Element of the carrier of (r,(r,X,D))
(X,D) is non empty strict TopSpace-like TopStruct
the carrier of (X,D) is non empty set
(X,D) is non empty Relation-like the carrier of X -defined the carrier of (X,D) -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of (X,D)) continuous Element of bool [: the carrier of X, the carrier of (X,D):]
[: the carrier of X, the carrier of (X,D):] is non empty Relation-like set
bool [: the carrier of X, the carrier of (X,D):] is non empty set
proj D is non empty Relation-like the carrier of X -defined D -valued Function-like V20( the carrier of X) V21( the carrier of X,D) Element of bool [: the carrier of X,D:]
[: the carrier of X,D:] is non empty Relation-like set
bool [: the carrier of X,D:] is non empty set
THETA is Element of the carrier of X
(X,D) . THETA is Element of the carrier of (X,D)
bool the carrier of X is non empty set
THETA is Element of bool the carrier of X
{II} is non empty trivial finite compact Element of bool the carrier of r
r is non empty TopSpace-like TopStruct
X is non empty TopSpace-like (r) SubSpace of r
D is non empty with_non-empty_elements (X) (X)
(X,D) is non empty strict TopSpace-like TopStruct
(r,X,D) is non empty with_non-empty_elements (r) (r)
the carrier of r is non empty set
the carrier of X is non empty set
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is set
D \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : not b<sub>1</sub> in the carrier of X } is non empty set
(r,(r,X,D)) is non empty strict TopSpace-like TopStruct
the topology of (r,(r,X,D)) is non empty Element of bool (bool the carrier of (r,(r,X,D)))
the carrier of (r,(r,X,D)) is non empty set
bool the carrier of (r,(r,X,D)) is non empty set
bool (bool the carrier of (r,(r,X,D))) is non empty set
bool (r,X,D) is non empty set
the topology 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
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (r,X,D) : union b<sub>1</sub> in the topology of r } is set
the topology of (X,D) is non empty Element of bool (bool the carrier of (X,D))
the carrier of (X,D) is non empty set
bool the carrier of (X,D) is non empty set
bool (bool the carrier of (X,D)) is non empty set
bool D is non empty set
the topology of X is non empty Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool D : union b<sub>1</sub> in the topology of X } is set
[#] (X,D) is non empty non proper open closed dense non boundary Element of bool the carrier of (X,D)
[#] (r,(r,X,D)) is non empty non proper open closed dense non boundary Element of bool the carrier of (r,(r,X,D))
CH1 is Element of bool the carrier of (X,D)
II is Element of bool D
union II is set
THETA is Element of bool the carrier of X
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
THETA is Element of bool the carrier of r
THETA /\ ([#] X) is Element of bool the carrier of X
THETA \ ([#] X) is Element of bool the carrier of r
{ {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : b<sub>1</sub> in THETA \ ([#] X) } is set
THETA9 is set
THETA99 is Element of the carrier of r
{THETA99} is non empty trivial finite compact Element of bool the carrier of r
CH1 \/ { {b<sub>1</sub>} where b<sub>1</sub> is Element of the carrier of r : b<sub>1</sub> in THETA \ ([#] X) } is set
THETA9 is Element of bool the carrier of (r,(r,X,D))
THETA9 /\ ([#] (X,D)) is Element of bool the carrier of (X,D)
THETA99 is set
W9 is set
T is set
{THETA99} is non empty trivial finite set
W9 is non empty trivial finite set
W is Element of the carrier of r
W9 is set
T is non empty trivial finite set
W is set
W9 is Element of the carrier of r
{W9} is non empty trivial finite compact Element of bool the carrier of r
union THETA9 is set
THETA99 is set
W is Element of the carrier of r
{W} is non empty trivial finite compact Element of bool the carrier of r
(r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of r, the carrier of (r,(r,X,D)):]
[: the carrier of r, the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,(r,X,D)):] is non empty set
proj (r,X,D) is non empty Relation-like the carrier of r -defined (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r,(r,X,D)) Element of bool [: the carrier of r,(r,X,D):]
[: the carrier of r,(r,X,D):] is non empty Relation-like set
bool [: the carrier of r,(r,X,D):] is non empty set
(r,(r,X,D)) . W is Element of the carrier of (r,(r,X,D))
II is Element of bool the carrier of (r,(r,X,D))
II /\ ([#] (X,D)) is Element of bool the carrier of (X,D)
union CH1 is set
THETA is set
union II is set
[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X
(union II) /\ ([#] X) is Element of bool the carrier of X
(r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of r, the carrier of (r,(r,X,D)):]
[: the carrier of r, the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,(r,X,D)):] is non empty set
proj (r,X,D) is non empty Relation-like the carrier of r -defined (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r,(r,X,D)) Element of bool [: the carrier of r,(r,X,D):]
[: the carrier of r,(r,X,D):] is non empty Relation-like set
bool [: the carrier of r,(r,X,D):] is non empty set
(r,(r,X,D)) . THETA is set
THETA is set
THETA is set
THETA is Element of bool (r,X,D)
union THETA is set
CH1 is TopSpace-like SubSpace of (r,(r,X,D))
II is Element of bool the carrier of (r,(r,X,D))
the carrier of CH1 is set
II ` is Element of bool the carrier of (r,(r,X,D))
the carrier of (r,(r,X,D)) \ II is set
union II is set
THETA is Element of bool the carrier of r
THETA ` is Element of bool the carrier of r
the carrier of r \ THETA is set
THETA is Element of bool (r,X,D)
union THETA is set
TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct
the carrier of RealSpace is non empty set
Family_open_set RealSpace is Element of bool (bool the carrier of RealSpace)
bool the carrier of RealSpace is non empty set
bool (bool the carrier of RealSpace) is non empty set
TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr RealSpace) is non empty set
bool the carrier of (TopSpaceMetr RealSpace) is non empty set
0 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() natural real ext-real Element of NAT
[.0,1.] is V29() V30() V31() Element of bool REAL
r is non empty Element of bool the carrier of (TopSpaceMetr RealSpace)
(TopSpaceMetr RealSpace) | r is non empty strict TopSpace-like SubSpace of TopSpaceMetr RealSpace
X is Element of bool the carrier of (TopSpaceMetr RealSpace)
(TopSpaceMetr RealSpace) | X is strict TopSpace-like SubSpace of TopSpaceMetr RealSpace
X is TopStruct
D is TopStruct
r is Element of bool the carrier of (TopSpaceMetr RealSpace)
(TopSpaceMetr RealSpace) | r is strict TopSpace-like SubSpace of TopSpaceMetr RealSpace
() is TopStruct
r is non empty Element of bool the carrier of (TopSpaceMetr RealSpace)
(TopSpaceMetr RealSpace) | r is non empty strict TopSpace-like SubSpace of TopSpaceMetr RealSpace
the carrier of () is non empty set
r is Element of bool the carrier of (TopSpaceMetr RealSpace)
(TopSpaceMetr RealSpace) | r is strict TopSpace-like SubSpace of TopSpaceMetr RealSpace
[#] () is non empty non proper open closed dense non boundary Element of bool the carrier of ()
bool the carrier of () is non empty set
() is Element of the carrier of ()
() is Element of the carrier of ()
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
X is non empty TopSpace-like SubSpace of r
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
r is non empty TopSpace-like TopStruct
r is non empty TopSpace-like TopStruct
X is non empty TopSpace-like (r) SubSpace of r
D is non empty with_non-empty_elements (X) (X)
(r,X,D) is non empty with_non-empty_elements (r) (r)
the carrier of r is non empty set
the carrier of X is non empty set
{ {b₁} where b₁ is Element of the carrier of r : not b₁ in the carrier of X } is set
D \/ { {b₁} where b₁ is Element of the carrier of r : not b₁ in the carrier of X } is non empty set
(r,(r,X,D)) is non empty strict TopSpace-like TopStruct
(r,X,D) is non empty strict TopSpace-like ((r,(r,X,D))) SubSpace of (r,(r,X,D))
[: 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
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:]
the carrier of (r,(r,X,D)) is non empty set
(r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of r, the carrier of (r,(r,X,D)):]
[: the carrier of r, the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,(r,X,D)):] is non empty set
proj (r,X,D) is non empty Relation-like the carrier of r -defined (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r,(r,X,D)) Element of bool [: the carrier of r,(r,X,D):]
[: the carrier of r,(r,X,D):] is non empty Relation-like set
bool [: the carrier of r,(r,X,D):] is non empty set
(X,D) is non empty strict TopSpace-like TopStruct
the carrier of (X,D) is non empty set
(X,D) is non empty Relation-like the carrier of X -defined the carrier of (X,D) -valued Function-like V20( the carrier of X) V21( the carrier of X, the carrier of (X,D)) continuous Element of bool [: the carrier of X, the carrier of (X,D):]
[: the carrier of X, the carrier of (X,D):] is non empty Relation-like set
bool [: the carrier of X, the carrier of (X,D):] is non empty set
proj D is non empty Relation-like the carrier of X -defined D -valued Function-like V20( the carrier of X) V21( the carrier of X,D) Element of bool [: the carrier of X,D:]
[: the carrier of X,D:] is non empty Relation-like set
bool [: the carrier of X,D:] is non empty set
(X,D) * CH1 is non empty Relation-like the carrier of r -defined the carrier of r -defined the carrier of (X,D) -valued the carrier of (X,D) -valued Function-like V20( the carrier of r) V20( the carrier of r) V21( the carrier of r, the carrier of (X,D)) V21( the carrier of r, the carrier of (X,D)) continuous Element of bool [: the carrier of r, the carrier of (X,D):]
[: the carrier of r, the carrier of (X,D):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (X,D):] is non empty set
II is Element of the carrier of r
(r,(r,X,D)) . II is Element of the carrier of (r,(r,X,D))
THETA is Element of the carrier of r
(r,(r,X,D)) . THETA is Element of the carrier of (r,(r,X,D))
((X,D) * CH1) . II is Element of the carrier of (X,D)
((X,D) * CH1) . THETA is Element of the carrier of (X,D)
CH1 . II is Element of the carrier of X
(X,D) . II is set
CH1 . THETA is Element of the carrier of X
(X,D) . THETA is set
the carrier of (r,X,D) is non empty set
[: the carrier of (r,(r,X,D)), the carrier of (r,X,D):] is non empty Relation-like set
bool [: the carrier of (r,(r,X,D)), the carrier of (r,X,D):] is non empty set
II is non empty Relation-like the carrier of (r,(r,X,D)) -defined the carrier of (r,X,D) -valued Function-like V20( the carrier of (r,(r,X,D))) V21( the carrier of (r,(r,X,D)), the carrier of (r,X,D)) Element of bool [: the carrier of (r,(r,X,D)), the carrier of (r,X,D):]
II * (r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,X,D)) Element of bool [: the carrier of r, the carrier of (r,X,D):]
[: the carrier of r, the carrier of (r,X,D):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,X,D):] is non empty set
THETA is non empty Relation-like the carrier of (r,(r,X,D)) -defined the carrier of (r,X,D) -valued Function-like V20( the carrier of (r,(r,X,D))) V21( the carrier of (r,(r,X,D)), the carrier of (r,X,D)) Element of bool [: the carrier of (r,(r,X,D)), the carrier of (r,X,D):]
THETA is Element of the carrier of (r,(r,X,D))
THETA . THETA is Element of the carrier of (r,X,D)
THETA9 is a_neighborhood of THETA . THETA
{THETA} is non empty trivial finite compact Element of bool the carrier of (r,(r,X,D))
bool the carrier of (r,(r,X,D)) is non empty set
(r,(r,X,D)) " {THETA} is Element of bool the carrier of r
bool the carrier of r is non empty set
(r,(r,X,D),(THETA . THETA),((X,D) * CH1),THETA9) is a_neighborhood of ((X,D) * CH1) " {(THETA . THETA)}
{(THETA . THETA)} is non empty trivial finite compact Element of bool the carrier of (r,X,D)
bool the carrier of (r,X,D) is non empty set
((X,D) * CH1) " {(THETA . THETA)} is Element of bool the carrier of r
THETA99 is a_neighborhood of (r,(r,X,D)) " {THETA}
(r,(r,X,D)) .: THETA99 is Element of bool the carrier of (r,(r,X,D))
W is a_neighborhood of THETA
W9 is a_neighborhood of THETA
THETA .: W9 is Element of bool the carrier of (r,X,D)
((X,D) * CH1) .: THETA99 is Element of bool the carrier of (X,D)
bool the carrier of (X,D) is non empty set
THETA is non empty Relation-like the carrier of (r,(r,X,D)) -defined the carrier of (r,X,D) -valued Function-like V20( the carrier of (r,(r,X,D))) V21( the carrier of (r,(r,X,D)), the carrier of (r,X,D)) continuous Element of bool [: the carrier of (r,(r,X,D)), the carrier of (r,X,D):]
THETA9 is Element of the carrier of (r,(r,X,D))
THETA . THETA9 is Element of the carrier of (r,X,D)
THETA99 is Element of the carrier of r
(r,(r,X,D)) . THETA99 is Element of the carrier of (r,(r,X,D))
CH1 . THETA99 is Element of the carrier of X
THETA * (r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,X,D)) Element of bool [: the carrier of r, the carrier of (r,X,D):]
(THETA * (r,(r,X,D))) . THETA99 is Element of the carrier of (r,X,D)
(X,D) . THETA99 is set
r is non empty TopSpace-like TopStruct
X is non empty TopSpace-like (r) SubSpace of r
D is non empty with_non-empty_elements (X) (X)
(r,X,D) is non empty with_non-empty_elements (r) (r)
the carrier of r is non empty set
the carrier of X is non empty set
{ {b₁} where b₁ is Element of the carrier of r : not b₁ in the carrier of X } is set
D \/ { {b₁} where b₁ is Element of the carrier of r : not b₁ in the carrier of X } is non empty set
(r,(r,X,D)) is non empty strict TopSpace-like TopStruct
(r,X,D) is non empty strict TopSpace-like ((r,(r,X,D))) SubSpace of (r,(r,X,D))
(r,()) is non empty strict TopSpace-like TopStruct
the carrier of (r,()) is non empty set
[: the carrier of (r,()), the carrier of r:] is non empty Relation-like set
bool [: the carrier of (r,()), the carrier of r:] is non empty set
CH1 is non empty Relation-like the carrier of (r,()) -defined the carrier of r -valued Function-like V20( the carrier of (r,())) V21( the carrier of (r,()), the carrier of r) continuous Element of bool [: the carrier of (r,()), the carrier of r:]
[: the carrier of r, the carrier of ():] is non empty Relation-like set
((r,(r,X,D)),()) is non empty strict TopSpace-like TopStruct
the carrier of ((r,(r,X,D)),()) is non empty set
[: the carrier of (r,()), the carrier of ((r,(r,X,D)),()):] is non empty Relation-like set
bool [: the carrier of (r,()), the carrier of ((r,(r,X,D)),()):] is non empty set
the carrier of (r,(r,X,D)) is non empty set
(r,(r,X,D)) is non empty Relation-like the carrier of r -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of r) V21( the carrier of r, the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of r, the carrier of (r,(r,X,D)):]
[: the carrier of r, the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of r, the carrier of (r,(r,X,D)):] is non empty set
proj (r,X,D) is non empty Relation-like the carrier of r -defined (r,X,D) -valued Function-like V20( the carrier of r) V21( the carrier of r,(r,X,D)) Element of bool [: the carrier of r,(r,X,D):]
[: the carrier of r,(r,X,D):] is non empty Relation-like set
bool [: the carrier of r,(r,X,D):] is non empty set
id the carrier of () is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like one-to-one V20( the carrier of ()) V21( the carrier of (), the carrier of ()) V22( the carrier of ()) V23( the carrier of (), the carrier of ()) V36() V38() V39() V43() Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty set
[:(r,(r,X,D)),(id the carrier of ()):] is non empty Relation-like [: the carrier of r, the carrier of ():] -defined [: the carrier of (r,(r,X,D)), the carrier of ():] -valued Function-like V20([: the carrier of r, the carrier of ():]) V21([: the carrier of r, the carrier of ():],[: the carrier of (r,(r,X,D)), the carrier of ():]) Element of bool [:[: the carrier of r, the carrier of ():],[: the carrier of (r,(r,X,D)), the carrier of ():]:]
[: the carrier of (r,(r,X,D)), the carrier of ():] is non empty Relation-like set
[:[: the carrier of r, the carrier of ():],[: the carrier of (r,(r,X,D)), the carrier of ():]:] is non empty Relation-like set
bool [:[: the carrier of r, the carrier of ():],[: the carrier of (r,(r,X,D)), the carrier of ():]:] is non empty set
II is non empty Relation-like the carrier of (r,()) -defined the carrier of ((r,(r,X,D)),()) -valued Function-like V20( the carrier of (r,())) V21( the carrier of (r,()), the carrier of ((r,(r,X,D)),())) Element of bool [: the carrier of (r,()), the carrier of ((r,(r,X,D)),()):]
(r,(r,X,D)) * CH1 is non empty Relation-like the carrier of (r,()) -defined the carrier of (r,()) -defined the carrier of (r,(r,X,D)) -valued the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of (r,())) V20( the carrier of (r,())) V21( the carrier of (r,()), the carrier of (r,(r,X,D))) V21( the carrier of (r,()), the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of (r,()), the carrier of (r,(r,X,D)):]
[: the carrier of (r,()), the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of (r,()), the carrier of (r,(r,X,D)):] is non empty set
THETA is Element of the carrier of (r,())
II . THETA is Element of the carrier of ((r,(r,X,D)),())
THETA is Element of the carrier of (r,())
II . THETA is Element of the carrier of ((r,(r,X,D)),())
((r,(r,X,D)) * CH1) . THETA is Element of the carrier of (r,(r,X,D))
((r,(r,X,D)) * CH1) . THETA is Element of the carrier of (r,(r,X,D))
CH1 . THETA is Element of the carrier of r
(r,(r,X,D)) . (CH1 . THETA) is Element of the carrier of (r,(r,X,D))
CH1 . THETA is Element of the carrier of r
(r,(r,X,D)) . (CH1 . THETA) is Element of the carrier of (r,(r,X,D))
THETA9 is Element of the carrier of r
THETA99 is Element of the carrier of ()
(r,(),THETA9,THETA99) is non empty V7() Element of the carrier of (r,())
{THETA9,THETA99} is non empty finite set
{THETA9} is non empty trivial finite set
{{THETA9,THETA99},{THETA9}} is non empty finite V28() set
W is Element of the carrier of r
W9 is Element of the carrier of ()
(r,(),W,W9) is non empty V7() Element of the carrier of (r,())
{W,W9} is non empty finite set
{W} is non empty trivial finite set
{{W,W9},{W}} is non empty finite V28() set
II . (THETA9,THETA99) is set
[THETA9,THETA99] is non empty V7() set
II . [THETA9,THETA99] is set
(r,(r,X,D)) . THETA9 is Element of the carrier of (r,(r,X,D))
((r,(r,X,D)),(),((r,(r,X,D)) . THETA9),THETA99) is non empty V7() Element of the carrier of ((r,(r,X,D)),())
{((r,(r,X,D)) . THETA9),THETA99} is non empty finite set
{((r,(r,X,D)) . THETA9)} is non empty trivial finite set
{{((r,(r,X,D)) . THETA9),THETA99},{((r,(r,X,D)) . THETA9)}} is non empty finite V28() set
II . (W,W9) is set
[W,W9] is non empty V7() set
II . [W,W9] is set
(r,(r,X,D)) . W is Element of the carrier of (r,(r,X,D))
((r,(r,X,D)),(),((r,(r,X,D)) . W),W9) is non empty V7() Element of the carrier of ((r,(r,X,D)),())
{((r,(r,X,D)) . W),W9} is non empty finite set
{((r,(r,X,D)) . W)} is non empty trivial finite set
{{((r,(r,X,D)) . W),W9},{((r,(r,X,D)) . W)}} is non empty finite V28() set
[: the carrier of ((r,(r,X,D)),()), the carrier of (r,(r,X,D)):] is non empty Relation-like set
bool [: the carrier of ((r,(r,X,D)),()), the carrier of (r,(r,X,D)):] is non empty set
THETA is non empty Relation-like the carrier of ((r,(r,X,D)),()) -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of ((r,(r,X,D)),())) V21( the carrier of ((r,(r,X,D)),()), the carrier of (r,(r,X,D))) Element of bool [: the carrier of ((r,(r,X,D)),()), the carrier of (r,(r,X,D)):]
THETA * II is non empty Relation-like the carrier of (r,()) -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of (r,())) V21( the carrier of (r,()), the carrier of (r,(r,X,D))) Element of bool [: the carrier of (r,()), the carrier of (r,(r,X,D)):]
THETA is non empty Relation-like the carrier of ((r,(r,X,D)),()) -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of ((r,(r,X,D)),())) V21( the carrier of ((r,(r,X,D)),()), the carrier of (r,(r,X,D))) Element of bool [: the carrier of ((r,(r,X,D)),()), the carrier of (r,(r,X,D)):]
THETA9 is Element of the carrier of ((r,(r,X,D)),())
THETA . THETA9 is Element of the carrier of (r,(r,X,D))
W is a_neighborhood of THETA . THETA9
T is Element of the carrier of (r,(r,X,D))
T is Element of the carrier of ()
((r,(r,X,D)),(),T,T) is non empty V7() Element of the carrier of ((r,(r,X,D)),())
{T,T} is non empty finite set
{T} is non empty trivial finite set
{{T,T},{T}} is non empty finite V28() set
THETA99 is Element of [: the carrier of (r,(r,X,D)), the carrier of ():]
{THETA99} is non empty trivial Relation-like the carrier of (r,(r,X,D)) -defined the carrier of () -valued finite Element of bool [: the carrier of (r,(r,X,D)), the carrier of ():]
bool [: the carrier of (r,(r,X,D)), the carrier of ():] is non empty set
II " {THETA99} is Element of bool the carrier of (r,())
bool the carrier of (r,()) is non empty set
{T} is non empty trivial finite compact Element of bool the carrier of (r,(r,X,D))
bool the carrier of (r,(r,X,D)) is non empty set
(r,(r,X,D)) " {T} is Element of bool the carrier of r
bool the carrier of r is non empty set
{T} is non empty trivial finite compact Element of bool the carrier of ()
bool the carrier of () is non empty set
(r,(),((r,(r,X,D)) " {T}),{T}) is Relation-like Element of bool the carrier of (r,())
W9 is non empty Relation-like the carrier of (r,()) -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of (r,())) V21( the carrier of (r,()), the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of (r,()), the carrier of (r,(r,X,D)):]
((r,()),(r,(r,X,D)),(THETA . THETA9),W9,W) is a_neighborhood of W9 " {(THETA . THETA9)}
{(THETA . THETA9)} is non empty trivial finite compact Element of bool the carrier of (r,(r,X,D))
W9 " {(THETA . THETA9)} is Element of bool the carrier of (r,())
GG is a_neighborhood of (r,(),((r,(r,X,D)) " {T}),{T})
U is a_neighborhood of (r,(r,X,D)) " {T}
V is a_neighborhood of T
(r,(),((r,(r,X,D)) " {T}),T,U,V) is Relation-like a_neighborhood of (r,(),((r,(r,X,D)) " {T}),{T})
(r,(r,X,D)) .: U is Element of bool the carrier of (r,(r,X,D))
H9 is a_neighborhood of T
((r,(r,X,D)),(),T,T,H9,V) is Relation-like a_neighborhood of ((r,(r,X,D)),(),T,T)
H99 is a_neighborhood of THETA9
H is a_neighborhood of THETA9
THETA .: H is Element of bool the carrier of (r,(r,X,D))
II .: (r,(),((r,(r,X,D)) " {T}),T,U,V) is Element of bool the carrier of ((r,(r,X,D)),())
bool the carrier of ((r,(r,X,D)),()) is non empty set
((r,(r,X,D)),(),((r,(r,X,D)) .: U),V) is Relation-like Element of bool the carrier of ((r,(r,X,D)),())
((r,(r,X,D)) * CH1) .: GG is Element of bool the carrier of (r,(r,X,D))
((r,(r,X,D)) * CH1) .: (r,(),((r,(r,X,D)) " {T}),T,U,V) is Element of bool the carrier of (r,(r,X,D))
THETA9 is non empty Relation-like the carrier of ((r,(r,X,D)),()) -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of ((r,(r,X,D)),())) V21( the carrier of ((r,(r,X,D)),()), the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of ((r,(r,X,D)),()), the carrier of (r,(r,X,D)):]
THETA99 is non empty Relation-like the carrier of ((r,(r,X,D)),()) -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of ((r,(r,X,D)),())) V21( the carrier of ((r,(r,X,D)),()), the carrier of (r,(r,X,D))) continuous Element of bool [: the carrier of ((r,(r,X,D)),()), the carrier of (r,(r,X,D)):]
the carrier of (r,X,D) is non empty set
W is Element of the carrier of (r,(r,X,D))
((r,(r,X,D)),(),W,()) is non empty V7() Element of the carrier of ((r,(r,X,D)),())
{W,()} is non empty finite set
{W} is non empty trivial finite set
{{W,()},{W}} is non empty finite V28() set
THETA99 . ((r,(r,X,D)),(),W,()) is Element of the carrier of (r,(r,X,D))
((r,(r,X,D)),(),W,()) is non empty V7() Element of the carrier of ((r,(r,X,D)),())
{W,()} is non empty finite set
{{W,()},{W}} is non empty finite V28() set
THETA99 . ((r,(r,X,D)),(),W,()) is Element of the carrier of (r,(r,X,D))
W9 is Element of the carrier of r
(r,(r,X,D)) . W9 is Element of the carrier of (r,(r,X,D))
II . (W9,()) is set
[W9,()] is non empty V7() set
{W9,()} is non empty finite set
{W9} is non empty trivial finite set
{{W9,()},{W9}} is non empty finite V28() set
II . [W9,()] is set
THETA9 * II is non empty Relation-like the carrier of (r,()) -defined the carrier of (r,(r,X,D)) -valued Function-like V20( the carrier of (r,())) V21( the carrier of (r,()), the carrier of (r,(r,X,D))) Element of bool [: the carrier of (r,()), the carrier of (r,(r,X,D)):]
(r,(),W9,()) is non empty V7() Element of the carrier of (r,())
(THETA9 * II) . (r,(),W9,()) is Element of the carrier of (r,(r,X,D))
THETA9 . ((r,(r,X,D)),(),W,()) is Element of the carrier of (r,(r,X,D))
CH1 . (W9,()) is set
CH1 . [W9,()] is set
(r,(),W9,()) is non empty V7() Element of the carrier of (r,())
{W9,()} is non empty finite set
{{W9,()},{W9}} is non empty finite V28() set
CH1 . (r,(),W9,()) is Element of the carrier of r
II . (W9,()) is set
[W9,()] is non empty V7() set
II . [W9,()] is set
(THETA9 * II) . (r,(),W9,()) is Element of the carrier of (r,(r,X,D))
THETA9 . ((r,(r,X,D)),(),W,()) is Element of the carrier of (r,(r,X,D))
(r,(r,X,D)) . (CH1 . (r,(),W9,())) is Element of the carrier of (r,(r,X,D))
T is Element of the carrier of ()
((r,(r,X,D)),(),W,T) is non empty V7() Element of the carrier of ((r,(r,X,D)),())
{W,T} is non empty finite set
{{W,T},{W}} is non empty finite V28() set
THETA99 . ((r,(r,X,D)),(),W,T) is Element of the carrier of (r,(r,X,D))
II . (W9,T) is set
[W9,T] is non empty V7() set
{W9,T} is non empty finite set
{{W9,T},{W9}} is non empty finite V28() set
II . [W9,T] is set
(r,(),W9,T) is non empty V7() Element of the carrier of (r,())
(THETA9 * II) . (r,(),W9,T) is Element of the carrier of (r,(r,X,D))
THETA9 . ((r,(r,X,D)),(),W,T) is Element of the carrier of (r,(r,X,D))
CH1 . (W9,T) is set
CH1 . [W9,T] is set
r is real ext-real set
{ b₁ where b₁ is real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
X is real ext-real Element of REAL