:: 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

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

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

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

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

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

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

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

{ (union b

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

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

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

(r,X,CH1) is open Element of bool (bool the carrier of (r,X))

{ (r,X,b

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

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

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

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

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

{ b

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