:: BORSUK_4 semantic presentation

REAL is V143() V144() V145() V149() non bounded_below non bounded_above interval set
NAT is V143() V144() V145() V146() V147() V148() V149() bounded_below Element of bool REAL
bool REAL is non empty set
omega is V143() V144() V145() V146() V147() V148() V149() bounded_below set
bool omega is non empty set
bool NAT is non empty set
1 is non empty natural V72() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is non empty set

bool is non empty set
2 is non empty natural V72() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
[:2,2:] is non empty set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is non empty set
COMPLEX is V143() V149() set
RAT is V143() V144() V145() V146() V149() set
INT is V143() V144() V145() V146() V147() V149() set
bool is non empty set

the carrier of () is functional non empty non trivial set
bool the carrier of () is non empty set

the carrier of I[01] is non empty V143() V144() V145() set
K199() is V85() V197() L7()

0 is empty trivial natural V72() real ext-real non positive non negative V80() V81() V143() V144() V145() V146() V147() V148() V149() bounded_below interval Element of NAT

the carrier of () is non empty V143() V144() V145() set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

[.0,1.] is V143() V144() V145() closed interval Element of bool REAL
the carrier of R^1 is non empty V143() V144() V145() set

the carrier of I[01] is non empty V143() V144() V145() set
bool the carrier of I[01] is non empty set
bool the carrier of R^1 is non empty set
(#) (0,1) is V72() real ext-real Element of the carrier of ()
(0,1) (#) is V72() real ext-real Element of the carrier of ()
bool the carrier of I[01] is non empty set
{0,1} is non empty V143() V144() V145() V146() V147() V148() left_end bounded_below set
the carrier of I[01] \ {0,1} is V143() V144() V145() Element of bool the carrier of I[01]

the carrier of () is non empty set

C is V35(2) V77() V135() Element of the carrier of ()
x is V35(2) V77() V135() Element of the carrier of ()
D is non empty set
bool D is non empty set
C is non empty Element of bool D
D is non empty non trivial set
C is set
{C} is non empty trivial set
D \ {C} is Element of bool D
bool D is non empty set
x is set
y is Element of D
D is non empty non trivial set
bool D is non empty set
C is non empty non trivial Element of bool D
x is set
{x} is non empty trivial set
C \ {x} is Element of bool D
y9 is set
Y is Element of D

dom D is set
dom C is set
(dom D) /\ (dom C) is set
rng D is set
rng C is set
(rng D) /\ (rng C) is set

x is set
{x} is non empty trivial set
D . x is set
{(D . x)} is non empty trivial set
(dom D) \ (dom C) is Element of bool (dom D)
bool (dom D) is non empty set
y is set
y9 is set
C . y is set
D . y9 is set

dom D is set
dom C is set
(dom D) /\ (dom C) is set
rng D is set
rng C is set
(rng D) /\ (rng C) is set

(D +* C) " is Relation-like Function-like set

(D ") +* (C ") is Relation-like Function-like set
x is set
{x} is non empty trivial set
D . x is set
{(D . x)} is non empty trivial set
C . x is set
dom (C ") is set
dom (D ") is set
(dom (D ")) /\ (dom (C ")) is set
y is set
(D ") . y is set
(C ") . y is set
Y is set
D . Y is set
C . Y is set
dom ((D ") +* (C ")) is set
(dom (D ")) \/ (dom (C ")) is set
(rng D) \/ (dom (C ")) is set
(rng D) \/ (rng C) is set
rng (D +* C) is set
dom (D +* C) is set
(dom D) \/ (dom C) is set
Y is set
Cy is set
((D ") +* (C ")) . Y is set
(D +* C) . Cy is set
(D ") . Y is set
D . Cy is set
(C ") . Y is set
C . Cy is set
D . Cy is set
(D ") . Y is set
C . Cy is set
(C ") . Y is set
D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

the carrier of () is functional non empty set
bool the carrier of () is non empty set
C is Element of bool the carrier of ()
x is V35(D) V77() V135() Element of the carrier of ()
y is V35(D) V77() V135() Element of the carrier of ()
{x} is non empty trivial closed compact bounded Element of bool the carrier of ()
C \ {x} is Element of bool the carrier of ()
{x,y} is non empty Element of bool the carrier of ()
C \ {x,y} is Element of bool the carrier of ()
D is V72() real ext-real set
C is V72() real ext-real set
x is V72() real ext-real set
y is V72() real ext-real set
1 - y is V72() real ext-real set
(1 - y) * C is V72() real ext-real set
y * x is V72() real ext-real set
((1 - y) * C) + (y * x) is V72() real ext-real set
(1 - y) * D is V72() real ext-real set
y * D is V72() real ext-real set
((1 - y) * D) + (y * D) is V72() real ext-real set
1 * D is V72() real ext-real set
D is V143() V144() V145() Element of bool the carrier of I[01]
x is V72() real ext-real set
C is V72() real ext-real set
].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
[.C,x.] is V143() V144() V145() closed interval Element of bool REAL
D is V143() V144() V145() Element of bool the carrier of I[01]
x is V72() real ext-real set
C is V72() real ext-real set
].C,x.] is V143() V144() V145() non left_end interval Element of bool REAL
[.C,x.] is V143() V144() V145() closed interval Element of bool REAL
].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
D is V143() V144() V145() Element of bool the carrier of I[01]
x is V72() real ext-real set
C is V72() real ext-real set
[.C,x.[ is V143() V144() V145() non right_end interval Element of bool REAL
[.C,x.] is V143() V144() V145() closed interval Element of bool REAL
].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
D is V72() real ext-real set
C is V72() real ext-real set
].D,C.] is V143() V144() V145() non left_end interval Element of bool REAL
Cl ].D,C.] is V143() V144() V145() Element of bool REAL
[.D,C.] is V143() V144() V145() closed interval Element of bool REAL
].D,C.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
Cl ].D,C.[ is V143() V144() V145() Element of bool REAL
D is V72() real ext-real set
C is V72() real ext-real set
[.D,C.[ is V143() V144() V145() non right_end interval Element of bool REAL
Cl [.D,C.[ is V143() V144() V145() Element of bool REAL
[.D,C.] is V143() V144() V145() closed interval Element of bool REAL
].D,C.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
Cl ].D,C.[ is V143() V144() V145() Element of bool REAL
D is V143() V144() V145() Element of bool the carrier of I[01]
Cl D is closed V143() V144() V145() Element of bool the carrier of I[01]
x is V72() real ext-real set
C is V72() real ext-real set
].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
[.C,x.] is V143() V144() V145() closed interval Element of bool REAL
Cl ].C,x.[ is V143() V144() V145() Element of bool REAL
y is V143() V144() V145() Element of bool the carrier of R^1
Cl y is closed V143() V144() V145() Element of bool the carrier of R^1
[#] I[01] is non empty non proper open closed V143() V144() V145() Element of bool the carrier of I[01]
(Cl y) /\ () is V143() V144() V145() Element of bool the carrier of I[01]
[.C,x.] /\ () is V143() V144() V145() Element of bool the carrier of I[01]
D is V143() V144() V145() Element of bool the carrier of I[01]
Cl D is closed V143() V144() V145() Element of bool the carrier of I[01]
x is V72() real ext-real set
C is V72() real ext-real set
].C,x.] is V143() V144() V145() non left_end interval Element of bool REAL
[.C,x.] is V143() V144() V145() closed interval Element of bool REAL
Cl ].C,x.] is V143() V144() V145() Element of bool REAL
y is V143() V144() V145() Element of bool the carrier of R^1
Cl y is closed V143() V144() V145() Element of bool the carrier of R^1
[#] I[01] is non empty non proper open closed V143() V144() V145() Element of bool the carrier of I[01]
(Cl y) /\ () is V143() V144() V145() Element of bool the carrier of I[01]
[.C,x.] /\ () is V143() V144() V145() Element of bool the carrier of I[01]
D is V143() V144() V145() Element of bool the carrier of I[01]
Cl D is closed V143() V144() V145() Element of bool the carrier of I[01]
x is V72() real ext-real set
C is V72() real ext-real set
[.C,x.[ is V143() V144() V145() non right_end interval Element of bool REAL
[.C,x.] is V143() V144() V145() closed interval Element of bool REAL
Cl [.C,x.[ is V143() V144() V145() Element of bool REAL
y is V143() V144() V145() Element of bool the carrier of R^1
Cl y is closed V143() V144() V145() Element of bool the carrier of R^1
[#] I[01] is non empty non proper open closed V143() V144() V145() Element of bool the carrier of I[01]
(Cl y) /\ () is V143() V144() V145() Element of bool the carrier of I[01]
[.C,x.] /\ () is V143() V144() V145() Element of bool the carrier of I[01]
D is V143() V144() V145() Element of bool the carrier of I[01]
C is V72() real ext-real set
x is V72() real ext-real set
[.C,x.] is V143() V144() V145() closed interval Element of bool REAL
D is V143() V144() V145() Element of bool the carrier of I[01]
C is V143() V144() V145() Element of bool the carrier of I[01]
y is V72() real ext-real set
x is V72() real ext-real set
y9 is V72() real ext-real set
[.x,y.[ is V143() V144() V145() non right_end interval Element of bool REAL
].y,y9.] is V143() V144() V145() non left_end interval Element of bool REAL
Cl D is closed V143() V144() V145() Element of bool the carrier of I[01]
[.x,y.] is V143() V144() V145() closed interval Element of bool REAL
Cl C is closed V143() V144() V145() Element of bool the carrier of I[01]
[.y,y9.] is V143() V144() V145() closed interval Element of bool REAL
D is V72() real ext-real Element of the carrier of I[01]
C is V72() real ext-real Element of the carrier of I[01]
[.D,C.] is V143() V144() V145() closed interval Element of bool REAL
D is V72() real ext-real Element of the carrier of I[01]
C is V72() real ext-real Element of the carrier of I[01]
].D,C.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
[.D,C.] is V143() V144() V145() closed interval Element of bool REAL
D is V72() real ext-real set
{D} is non empty trivial V143() V144() V145() Element of bool REAL
[.D,D.] is V143() V144() V145() closed interval Element of bool REAL
D is non empty connected V143() V144() V145() Element of bool the carrier of I[01]
C is V72() real ext-real Element of the carrier of I[01]
x is V72() real ext-real Element of the carrier of I[01]
y is V72() real ext-real Element of the carrier of I[01]
].x,1.] is V143() V144() V145() non left_end interval Element of bool REAL
[.x,1.] is V143() V144() V145() closed interval Element of bool REAL
[.0,x.[ is V143() V144() V145() non right_end interval Element of bool REAL
[.0,x.] is V143() V144() V145() closed interval Element of bool REAL
{x} is non empty trivial V143() V144() V145() Element of bool REAL
[.0,1.] \ {x} is V143() V144() V145() Element of bool REAL
[.0,x.[ \/ ].x,1.] is V143() V144() V145() Element of bool REAL
y9 is non empty V143() V144() V145() Element of bool the carrier of I[01]
Y is non empty V143() V144() V145() Element of bool the carrier of I[01]
y9 is non empty V143() V144() V145() Element of bool the carrier of I[01]
Y is non empty V143() V144() V145() Element of bool the carrier of I[01]
D is non empty connected V143() V144() V145() Element of bool the carrier of I[01]
C is V72() real ext-real set
x is V72() real ext-real set
[.C,x.] is V143() V144() V145() closed interval Element of bool REAL
y is set
{ b1 where b1 is V72() real ext-real Element of REAL : ( C <= b1 & b1 <= x ) } is set
y9 is V72() real ext-real Element of REAL
Y is V72() real ext-real Element of the carrier of I[01]
D is V72() real ext-real set
C is V72() real ext-real set
[.D,C.] is V143() V144() V145() closed interval Element of bool REAL
x is V143() V144() V145() Element of bool the carrier of I[01]
Closed-Interval-TSpace (D,C) is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of R^1
bool the carrier of () is non empty set
the carrier of () is non empty V143() V144() V145() set
y is V143() V144() V145() Element of bool the carrier of ()

D is V72() real ext-real Element of the carrier of I[01]
C is V72() real ext-real Element of the carrier of I[01]
[.D,C.] is V143() V144() V145() closed interval Element of bool REAL
Closed-Interval-TSpace (D,C) is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of R^1
y is V143() V144() V145() Element of bool the carrier of I[01]

D is V143() V144() V145() Element of bool the carrier of I[01]
C is V143() V144() V145() Element of bool REAL
x is ext-real set
x is ext-real set
D is V143() V144() V145() Element of bool the carrier of I[01]
C is V143() V144() V145() Element of bool REAL

x is V72() real ext-real set
C is V143() V144() V145() Element of bool REAL
x is V143() V144() V145() Element of bool the carrier of I[01]
y is V143() V144() V145() Element of bool the carrier of R^1
[#] I[01] is non empty non proper open closed V143() V144() V145() Element of bool the carrier of I[01]
y /\ () is V143() V144() V145() Element of bool the carrier of I[01]
D is V143() V144() V145() Element of bool the carrier of R^1
D is non empty V143() V144() V145() closed_interval interval Element of bool REAL

the V72() real ext-real Element of D is V72() real ext-real Element of D
D is non empty closed connected compact V143() V144() V145() Element of bool the carrier of I[01]
C is V143() V144() V145() Element of bool REAL

[.(),().] is V143() V144() V145() closed interval Element of bool REAL
x is set
y is V72() real ext-real set
D is non empty closed connected compact V143() V144() V145() Element of bool the carrier of I[01]
C is V143() V144() V145() Element of bool REAL

[.(),().] is V143() V144() V145() closed interval Element of bool REAL
D is non empty closed connected compact V143() V144() V145() Element of bool the carrier of I[01]
C is non empty V143() V144() V145() closed_interval interval Element of bool REAL

[.(),().] is V143() V144() V145() closed interval Element of bool REAL
x is V72() real ext-real Element of the carrier of I[01]
y is V72() real ext-real Element of the carrier of I[01]
[.x,y.] is V143() V144() V145() closed interval Element of bool REAL
].0,1.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
D is V143() V144() V145() Element of bool the carrier of I[01]

the carrier of () is V143() V144() V145() set

the carrier of D is V143() V144() V145() set

the carrier of C is V143() V144() V145() set

the carrier of () is V143() V144() V145() set
the carrier of () is non empty V143() V144() V145() set
D is V143() V144() V145() Element of bool the carrier of I[01]

the carrier of I[01] \ {0,1} is V143() V144() V145() Element of bool the carrier of I[01]
].0,1.[ \/ {0,1} is non empty V143() V144() V145() set
D is V72() real ext-real set
bool the carrier of () is non empty set
C is V72() real ext-real Element of the carrier of I[01]
D is V72() real ext-real Element of the carrier of I[01]
].D,C.] is V143() V144() V145() non left_end interval Element of bool REAL
x is set
{ b1 where b1 is V72() real ext-real Element of REAL : ( not b1 <= D & b1 <= C ) } is set
y is V72() real ext-real Element of REAL
C is V72() real ext-real Element of the carrier of I[01]
D is V72() real ext-real Element of the carrier of I[01]
[.D,C.[ is V143() V144() V145() non right_end interval Element of bool REAL
x is set
{ b1 where b1 is V72() real ext-real Element of REAL : ( D <= b1 & not C <= b1 ) } is set
y is V72() real ext-real Element of REAL
D is non empty non trivial closed connected compact bounded being_simple_closed_curve Element of bool the carrier of ()
() | D is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of (() | D) is non empty set
[: the carrier of (), the carrier of (() | D):] is non empty set
bool [: the carrier of (), the carrier of (() | D):] is non empty set
C is Relation-like the carrier of () -defined the carrier of (() | D) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (), the carrier of (() | D):]
C is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

the carrier of () is functional non empty set
bool the carrier of () is non empty set
x is non empty Element of bool the carrier of ()
y is V35(C) V77() V135() Element of the carrier of ()
y9 is V35(C) V77() V135() Element of the carrier of ()
{y,y9} is non empty Element of bool the carrier of ()
x \ {y,y9} is Element of bool the carrier of ()
() | (x \ {y,y9}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C
() | x is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C
the carrier of (() | x) is non empty set
[: the carrier of I[01], the carrier of (() | x):] is non empty set
bool [: the carrier of I[01], the carrier of (() | x):] is non empty set
Y is Relation-like the carrier of I[01] -defined the carrier of (() | x) -valued Function-like non empty total quasi_total Element of bool [: the carrier of I[01], the carrier of (() | x):]
Y . 0 is set
Y . 1 is set
rng Y is Element of bool the carrier of (() | x)
bool the carrier of (() | x) is non empty set
[#] (() | x) is non empty non proper open closed Element of bool the carrier of (() | x)
dom Y is V143() V144() V145() Element of bool the carrier of I[01]
Y .: the carrier of () is Element of bool the carrier of (() | x)
Y .: the carrier of I[01] is Element of bool the carrier of (() | x)
Y .: {0,1} is Element of bool the carrier of (() | x)
(Y .: the carrier of I[01]) \ (Y .: {0,1}) is Element of bool the carrier of (() | x)
x \ (Y .: {0,1}) is Element of bool the carrier of ()
p1 is non empty Element of bool the carrier of ()
() | p1 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C
Cy is Element of bool the carrier of (() | x)
(() | x) | Cy is strict TopSpace-like T_0 T_1 T_2 SubSpace of () | x
Y /" is Relation-like the carrier of (() | x) -defined the carrier of I[01] -valued Function-like non empty total quasi_total Element of bool [: the carrier of (() | x), the carrier of I[01]:]
[: the carrier of (() | x), the carrier of I[01]:] is non empty set
bool [: the carrier of (() | x), the carrier of I[01]:] is non empty set
(Y /") | p1 is Relation-like the carrier of (() | x) -defined the carrier of I[01] -valued Function-like Element of bool [: the carrier of (() | x), the carrier of I[01]:]
the carrier of (() | p1) is non empty set
[: the carrier of (() | p1), the carrier of I[01]:] is non empty set
bool [: the carrier of (() | p1), the carrier of I[01]:] is non empty set
B is Relation-like the carrier of (() | p1) -defined the carrier of I[01] -valued Function-like non empty total quasi_total Element of bool [: the carrier of (() | p1), the carrier of I[01]:]
Y | the carrier of () is Relation-like the carrier of I[01] -defined the carrier of (() | x) -valued Function-like Element of bool [: the carrier of I[01], the carrier of (() | x):]
D is V143() V144() V145() Element of bool the carrier of I[01]

the carrier of () is V143() V144() V145() set
[: the carrier of (), the carrier of (() | x):] is set
bool [: the carrier of (), the carrier of (() | x):] is non empty set
dom (Y | the carrier of ()) is V143() V144() V145() Element of bool the carrier of I[01]

rng (Y | the carrier of ()) is Element of bool the carrier of (() | x)
the carrier of (() | (x \ {y,y9})) is set
[: the carrier of (), the carrier of (() | (x \ {y,y9})):] is set
bool [: the carrier of (), the carrier of (() | (x \ {y,y9})):] is non empty set
fC9 is Relation-like the carrier of () -defined the carrier of (() | (x \ {y,y9})) -valued Function-like quasi_total Element of bool [: the carrier of (), the carrier of (() | (x \ {y,y9})):]
dom fC9 is V143() V144() V145() Element of bool the carrier of ()
[#] () is non empty non proper open closed V143() V144() V145() Element of bool the carrier of ()
fC9 /" is Relation-like the carrier of (() | (x \ {y,y9})) -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of (() | (x \ {y,y9})), the carrier of ():]
[: the carrier of (() | (x \ {y,y9})), the carrier of ():] is set
bool [: the carrier of (() | (x \ {y,y9})), the carrier of ():] is non empty set

fC9 is Relation-like the carrier of () -defined the carrier of (() | x) -valued Function-like total quasi_total Element of bool [: the carrier of (), the carrier of (() | x):]
rng fC9 is Element of bool the carrier of (() | (x \ {y,y9}))
bool the carrier of (() | (x \ {y,y9})) is non empty set
[#] (() | (x \ {y,y9})) is non proper open closed Element of bool the carrier of (() | (x \ {y,y9}))
D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

the carrier of () is functional non empty set
bool the carrier of () is non empty set
C is Element of bool the carrier of ()

x is V35(D) V77() V135() Element of the carrier of ()
y is V35(D) V77() V135() Element of the carrier of ()
the carrier of (() | C) is set
[: the carrier of I[01], the carrier of (() | C):] is set
bool [: the carrier of I[01], the carrier of (() | C):] is non empty set
y9 is Relation-like the carrier of I[01] -defined the carrier of (() | C) -valued Function-like quasi_total Element of bool [: the carrier of I[01], the carrier of (() | C):]
y9 . 0 is set
y9 . 1 is set
D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

the carrier of () is functional non empty set
C is V35(D) V77() V135() Element of the carrier of ()
x is V35(D) V77() V135() Element of the carrier of ()
LSeg (C,x) is Element of bool the carrier of ()
bool the carrier of () is non empty set
() | (LSeg (C,x)) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
D is V143() V144() V145() Element of bool the carrier of ()
() | D is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of ()
x is V72() real ext-real Element of the carrier of I[01]
C is V72() real ext-real Element of the carrier of I[01]
[.C,x.] is V143() V144() V145() closed interval Element of bool REAL
Closed-Interval-TSpace (C,x) is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of R^1

the carrier of y is V143() V144() V145() set

(#) (C,x) is V72() real ext-real Element of the carrier of ()
the carrier of () is non empty V143() V144() V145() set
(C,x) (#) is V72() real ext-real Element of the carrier of ()
L[01] (((#) (C,x)),((C,x) (#))) is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

the carrier of () is functional non empty set
bool the carrier of () is non empty set
C is Element of bool the carrier of ()

the carrier of (() | C) is set
x is V35(D) V77() V135() Element of the carrier of ()
y is V35(D) V77() V135() Element of the carrier of ()
Y is V72() real ext-real Element of the carrier of I[01]
y9 is V72() real ext-real Element of the carrier of I[01]
[.y9,Y.] is V143() V144() V145() closed interval Element of bool REAL
Cy is non empty V143() V144() V145() Element of bool the carrier of I[01]
I[01] | Cy is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]
Closed-Interval-TSpace (y9,Y) is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of R^1
the carrier of (I[01] | Cy) is non empty V143() V144() V145() set
[: the carrier of (I[01] | Cy), the carrier of I[01]:] is non empty set
bool [: the carrier of (I[01] | Cy), the carrier of I[01]:] is non empty set
P[01] (y9,Y,((#) (0,1)),((0,1) (#))) is Relation-like the carrier of (Closed-Interval-TSpace (y9,Y)) -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (y9,Y)), the carrier of ():]
the carrier of (Closed-Interval-TSpace (y9,Y)) is non empty V143() V144() V145() set
[: the carrier of (Closed-Interval-TSpace (y9,Y)), the carrier of ():] is non empty set
bool [: the carrier of (Closed-Interval-TSpace (y9,Y)), the carrier of ():] is non empty set
[: the carrier of (I[01] | Cy), the carrier of (() | C):] is set
bool [: the carrier of (I[01] | Cy), the carrier of (() | C):] is non empty set
(#) (y9,Y) is V72() real ext-real Element of the carrier of (Closed-Interval-TSpace (y9,Y))
p2 is non empty Element of bool the carrier of ()
() | p2 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of (() | p2) is non empty set
[: the carrier of I[01], the carrier of (() | p2):] is non empty set
bool [: the carrier of I[01], the carrier of (() | p2):] is non empty set
B is Relation-like the carrier of I[01] -defined the carrier of (() | p2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of I[01], the carrier of (() | p2):]
B . 0 is set
B . 1 is set
p1 is Relation-like the carrier of (I[01] | Cy) -defined the carrier of I[01] -valued Function-like non empty total quasi_total Element of bool [: the carrier of (I[01] | Cy), the carrier of I[01]:]
B * p1 is Relation-like the carrier of (I[01] | Cy) -defined the carrier of (() | p2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (I[01] | Cy), the carrier of (() | p2):]
[: the carrier of (I[01] | Cy), the carrier of (() | p2):] is non empty set
bool [: the carrier of (I[01] | Cy), the carrier of (() | p2):] is non empty set
fC9 is Relation-like the carrier of (I[01] | Cy) -defined the carrier of (() | C) -valued Function-like quasi_total Element of bool [: the carrier of (I[01] | Cy), the carrier of (() | C):]
fC9 . y9 is set
fC9 . Y is set
p1 . y9 is set
B . (p1 . y9) is set
(y9,Y) (#) is V72() real ext-real Element of the carrier of (Closed-Interval-TSpace (y9,Y))
p1 . Y is set
B . (p1 . Y) is set

the carrier of D is set
bool the carrier of D is non empty set
C is non empty TopSpace-like TopStruct
the carrier of C is non empty set
[: the carrier of D, the carrier of C:] is set
bool [: the carrier of D, the carrier of C:] is non empty set
x is Relation-like the carrier of D -defined the carrier of C -valued Function-like total quasi_total Element of bool [: the carrier of D, the carrier of C:]

the carrier of y is set
y9 is Element of bool the carrier of D
D | y9 is strict TopSpace-like SubSpace of D
the carrier of (D | y9) is set
[: the carrier of (D | y9), the carrier of y:] is set
bool [: the carrier of (D | y9), the carrier of y:] is non empty set
x | y9 is Relation-like the carrier of D -defined the carrier of C -valued Function-like Element of bool [: the carrier of D, the carrier of C:]
[: the carrier of (D | y9), the carrier of C:] is set
bool [: the carrier of (D | y9), the carrier of C:] is non empty set
Cy is Relation-like the carrier of (D | y9) -defined the carrier of y -valued Function-like quasi_total Element of bool [: the carrier of (D | y9), the carrier of y:]
Y is Relation-like the carrier of (D | y9) -defined the carrier of C -valued Function-like total quasi_total Element of bool [: the carrier of (D | y9), the carrier of C:]
D is V143() V144() V145() Element of bool the carrier of I[01]
C is V72() real ext-real Element of the carrier of I[01]
x is V72() real ext-real Element of the carrier of I[01]
].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
[.x,1.] is V143() V144() V145() closed interval Element of bool REAL
[.0,C.] is V143() V144() V145() closed interval Element of bool REAL
y is V143() V144() V145() Element of bool the carrier of I[01]
y9 is V143() V144() V145() Element of bool the carrier of I[01]
y9 \/ y is V143() V144() V145() Element of bool the carrier of I[01]
(y9 \/ y) ` is V143() V144() V145() Element of bool the carrier of I[01]
the carrier of I[01] \ (y9 \/ y) is V143() V144() V145() set
D is V143() V144() V145() Element of bool the carrier of ()
C is V72() real ext-real Element of the carrier of I[01]
x is V72() real ext-real Element of the carrier of I[01]
].C,x.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
y is V143() V144() V145() Element of bool the carrier of I[01]
D is V143() V144() V145() Element of bool the carrier of ()
C is V72() real ext-real Element of the carrier of I[01]
].0,C.] is V143() V144() V145() non left_end interval Element of bool REAL
[#] () is non empty non proper open closed V143() V144() V145() Element of bool the carrier of ()
([#] ()) \ D is V143() V144() V145() Element of bool the carrier of ()
].C,1.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
{} () is empty trivial proper open closed connected compact V143() V144() V145() V146() V147() V148() V149() bounded_below interval Element of bool the carrier of ()
D is V143() V144() V145() Element of bool the carrier of ()
C is V72() real ext-real Element of the carrier of I[01]
[.C,1.[ is V143() V144() V145() non right_end interval Element of bool REAL
[#] () is non empty non proper open closed V143() V144() V145() Element of bool the carrier of ()
([#] ()) \ D is V143() V144() V145() Element of bool the carrier of ()
].0,C.[ is V143() V144() V145() open non left_end non right_end interval Element of bool REAL
D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

the carrier of () is functional non empty set
bool the carrier of () is non empty set
C is Element of bool the carrier of ()
x is V35(D) V77() V135() Element of the carrier of ()
y is V35(D) V77() V135() Element of the carrier of ()
{x} is non empty trivial closed compact bounded Element of bool the carrier of ()
C \ {x} is Element of bool the carrier of ()
() | (C \ {x}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of (() | (C \ {x})) is set
Y is V72() real ext-real Element of the carrier of I[01]
y9 is V72() real ext-real Element of the carrier of I[01]
].y9,Y.] is V143() V144() V145() non left_end interval Element of bool REAL
Cy is non empty Element of bool the carrier of ()
() | Cy is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of (() | Cy) is non empty set
[.y9,Y.] is V143() V144() V145() closed interval Element of bool REAL
p1 is non empty V143() V144() V145() Element of bool the carrier of I[01]
I[01] | p1 is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]
the carrier of (I[01] | p1) is non empty V143() V144() V145() set
[: the carrier of (I[01] | p1), the carrier of (() | Cy):] is non empty set
bool [: the carrier of (I[01] | p1), the carrier of (() | Cy):] is non empty set
p2 is Relation-like the carrier of (I[01] | p1) -defined the carrier of (() | Cy) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (I[01] | p1), the carrier of (() | Cy):]
p2 . y9 is set
p2 . Y is set
dom p2 is V143() V144() V145() Element of bool the carrier of (I[01] | p1)
bool the carrier of (I[01] | p1) is non empty set
[#] (I[01] | p1) is non empty non proper open closed V143() V144() V145() Element of bool the carrier of (I[01] | p1)
B is non empty V143() V144() V145() Element of bool the carrier of ()
() | B is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of ()
p2 | B is Relation-like the carrier of (I[01] | p1) -defined the carrier of (() | Cy) -valued Function-like Element of bool [: the carrier of (I[01] | p1), the carrier of (() | Cy):]
p2 /" is Relation-like the carrier of (() | Cy) -defined the carrier of (I[01] | p1) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (() | Cy), the carrier of (I[01] | p1):]
[: the carrier of (() | Cy), the carrier of (I[01] | p1):] is non empty set
bool [: the carrier of (() | Cy), the carrier of (I[01] | p1):] is non empty set

the carrier of (() | C) is set
bool the carrier of (() | C) is non empty set
p1 is V143() V144() V145() Element of bool the carrier of (I[01] | p1)
(I[01] | p1) | p1 is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01] | p1
the carrier of (() | B) is non empty V143() V144() V145() set
fC9 is Element of bool the carrier of (() | C)
(() | C) | fC9 is strict TopSpace-like T_0 T_1 T_2 SubSpace of () | C
dom (p2 | B) is V143() V144() V145() Element of bool the carrier of (I[01] | p1)
[#] (() | B) is non empty non proper open closed V143() V144() V145() Element of bool the carrier of (() | B)
bool the carrier of (() | B) is non empty set
rng p2 is Element of bool the carrier of (() | Cy)
bool the carrier of (() | Cy) is non empty set
[#] (() | C) is non proper open closed Element of bool the carrier of (() | C)
{y9} is non empty trivial V143() V144() V145() Element of bool REAL
p1 \ {y9} is V143() V144() V145() Element of bool the carrier of I[01]
p2 .: B is Element of bool the carrier of (() | Cy)
p2 .: p1 is Element of bool the carrier of (() | Cy)
Im (p2,y9) is set
{y9} is non empty trivial V143() V144() V145() set
p2 .: {y9} is set
(p2 .: p1) \ (Im (p2,y9)) is Element of bool the carrier of (() | Cy)
{(p2 . y9)} is non empty trivial set
(p2 .: p1) \ {(p2 . y9)} is Element of bool the carrier of (() | Cy)
(rng p2) \ {x} is Element of bool the carrier of (() | Cy)
[#] (() | (C \ {x})) is non proper open closed Element of bool the carrier of (() | (C \ {x}))
bool the carrier of (() | (C \ {x})) is non empty set
rng (p2 | B) is Element of bool the carrier of (() | Cy)
[: the carrier of (() | B), the carrier of (() | (C \ {x})):] is set
bool [: the carrier of (() | B), the carrier of (() | (C \ {x})):] is non empty set
p2 is Relation-like the carrier of (() | B) -defined the carrier of (() | (C \ {x})) -valued Function-like quasi_total Element of bool [: the carrier of (() | B), the carrier of (() | (C \ {x})):]
p2 . Y is set
p2 /" is Relation-like the carrier of (() | (C \ {x})) -defined the carrier of (() | B) -valued Function-like total quasi_total Element of bool [: the carrier of (() | (C \ {x})), the carrier of (() | B):]
[: the carrier of (() | (C \ {x})), the carrier of (() | B):] is set
bool [: the carrier of (() | (C \ {x})), the carrier of (() | B):] is non empty set

(p2 ") | (p2 .: B) is Relation-like set
(p2 /") | ([#] (() | (C \ {x}))) is Relation-like the carrier of (() | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of (() | Cy), the carrier of (I[01] | p1):]
(p2 /") | fC9 is Relation-like the carrier of (() | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of (() | Cy), the carrier of (I[01] | p1):]
D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

the carrier of () is functional non empty set
bool the carrier of () is non empty set
C is Element of bool the carrier of ()
x is V35(D) V77() V135() Element of the carrier of ()
y is V35(D) V77() V135() Element of the carrier of ()
{y} is non empty trivial closed compact bounded Element of bool the carrier of ()
C \ {y} is Element of bool the carrier of ()
() | (C \ {y}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of (() | (C \ {y})) is set
Y is V72() real ext-real Element of the carrier of I[01]
y9 is V72() real ext-real Element of the carrier of I[01]
[.y9,Y.[ is V143() V144() V145() non right_end interval Element of bool REAL
Cy is non empty Element of bool the carrier of ()
() | Cy is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of (() | Cy) is non empty set
[.y9,Y.] is V143() V144() V145() closed interval Element of bool REAL
p1 is non empty V143() V144() V145() Element of bool the carrier of I[01]
I[01] | p1 is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]
the carrier of (I[01] | p1) is non empty V143() V144() V145() set
[: the carrier of (I[01] | p1), the carrier of (() | Cy):] is non empty set
bool [: the carrier of (I[01] | p1), the carrier of (() | Cy):] is non empty set
p2 is Relation-like the carrier of (I[01] | p1) -defined the carrier of (() | Cy) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (I[01] | p1), the carrier of (() | Cy):]
p2 . y9 is set
p2 . Y is set
dom p2 is V143() V144() V145() Element of bool the carrier of (I[01] | p1)
bool the carrier of (I[01] | p1) is non empty set
[#] (I[01] | p1) is non empty non proper open closed V143() V144() V145() Element of bool the carrier of (I[01] | p1)
B is non empty V143() V144() V145() Element of bool the carrier of ()
() | B is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of ()
p2 | B is Relation-like the carrier of (I[01] | p1) -defined the carrier of (() | Cy) -valued Function-like Element of bool [: the carrier of (I[01] | p1), the carrier of (() | Cy):]
p2 /" is Relation-like the carrier of (() | Cy) -defined the carrier of (I[01] | p1) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (() | Cy), the carrier of (I[01] | p1):]
[: the carrier of (() | Cy), the carrier of (I[01] | p1):] is non empty set
bool [: the carrier of (() | Cy), the carrier of (I[01] | p1):] is non empty set

the carrier of (() | C) is set
bool the carrier of (() | C) is non empty set
p1 is V143() V144() V145() Element of bool the carrier of (I[01] | p1)
(I[01] | p1) | p1 is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01] | p1
the carrier of (() | B) is non empty V143() V144() V145() set
fC9 is Element of bool the carrier of (() | C)
(() | C) | fC9 is strict TopSpace-like T_0 T_1 T_2 SubSpace of () | C
dom (p2 | B) is V143() V144() V145() Element of bool the carrier of (I[01] | p1)
[#] (() | B) is non empty non proper open closed V143() V144() V145() Element of bool the carrier of (() | B)
bool the carrier of (() | B) is non empty set
rng p2 is Element of bool the carrier of (() | Cy)
bool the carrier of (() | Cy) is non empty set
[#] (() | C) is non proper open closed Element of bool the carrier of (() | C)
{Y} is non empty trivial V143() V144() V145() Element of bool REAL
p1 \ {Y} is V143() V144() V145() Element of bool the carrier of I[01]
p2 .: B is Element of bool the carrier of (() | Cy)
p2 .: p1 is Element of bool the carrier of (() | Cy)
Im (p2,Y) is set
{Y} is non empty trivial V143() V144() V145() set
p2 .: {Y} is set
(p2 .: p1) \ (Im (p2,Y)) is Element of bool the carrier of (() | Cy)
{(p2 . Y)} is non empty trivial set
(p2 .: p1) \ {(p2 . Y)} is Element of bool the carrier of (() | Cy)
(rng p2) \ {y} is Element of bool the carrier of (() | Cy)
[#] (() | (C \ {y})) is non proper open closed Element of bool the carrier of (() | (C \ {y}))
bool the carrier of (() | (C \ {y})) is non empty set
rng (p2 | B) is Element of bool the carrier of (() | Cy)
[: the carrier of (() | B), the carrier of (() | (C \ {y})):] is set
bool [: the carrier of (() | B), the carrier of (() | (C \ {y})):] is non empty set
p2 is Relation-like the carrier of (() | B) -defined the carrier of (() | (C \ {y})) -valued Function-like quasi_total Element of bool [: the carrier of (() | B), the carrier of (() | (C \ {y})):]
p2 . y9 is set
p2 /" is Relation-like the carrier of (() | (C \ {y})) -defined the carrier of (() | B) -valued Function-like total quasi_total Element of bool [: the carrier of (() | (C \ {y})), the carrier of (() | B):]
[: the carrier of (() | (C \ {y})), the carrier of (() | B):] is set
bool [: the carrier of (() | (C \ {y})), the carrier of (() | B):] is non empty set

(p2 ") | (p2 .: B) is Relation-like set
(p2 /") | ([#] (() | (C \ {y}))) is Relation-like the carrier of (() | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of (() | Cy), the carrier of (I[01] | p1):]
(p2 /") | fC9 is Relation-like the carrier of (() | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of (() | Cy), the carrier of (I[01] | p1):]
1 / 2 is V72() real ext-real non negative set
y is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

the carrier of () is functional non empty set
bool the carrier of () is non empty set
y9 is Element of bool the carrier of ()
Y is Element of bool the carrier of ()
y9 /\ Y is Element of bool the carrier of ()
Cy is V35(y) V77() V135() Element of the carrier of ()
p1 is V35(y) V77() V135() Element of the carrier of ()
{Cy,p1} is non empty Element of bool the carrier of ()
{Cy} is non empty trivial closed compact bounded Element of bool the carrier of ()
y9 \ {Cy} is Element of bool the carrier of ()
Y \ {Cy} is Element of bool the carrier of ()
(y9 \ {Cy}) \/ (Y \ {Cy}) is Element of bool the carrier of ()
() | ((y9 \ {Cy}) \/ (Y \ {Cy})) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y
() | (Y \ {Cy}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y
the carrier of (() | (Y \ {Cy})) is set
C is V72() real ext-real Element of the carrier of I[01]
x is V72() real ext-real Element of the carrier of I[01]
[.C,x.[ is V143() V144() V145() non right_end interval Element of bool REAL
p2 is non empty V143() V144() V145() Element of bool the carrier of ()
() | p2 is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of ()
the carrier of (() | p2) is non empty V143() V144() V145() set
[: the carrier of (() | p2), the carrier of (() | (Y \ {Cy})):] is set
bool [: the carrier of (() | p2), the carrier of (() | (Y \ {Cy})):] is non empty set
B is Relation-like the carrier of (() | p2) -defined the carrier of (() | (Y \ {Cy})) -valued Function-like quasi_total Element of bool [: the carrier of (() | p2), the carrier of (() | (Y \ {Cy})):]
B . C is set
() | (y9 \ {Cy}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y
the carrier of (() | (y9 \ {Cy})) is set
D is V72() real ext-real Element of the carrier of I[01]
].D,C.] is V143() V144() V145() non left_end interval Element of bool REAL
c11 is non empty V143() V144() V145() Element of bool the carrier of ()
() | c11 is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of ()
the carrier of (() | c11) is non empty V143() V144() V145() set
[: the carrier of (() | c11), the carrier of (() | (y9 \ {Cy})):] is set
bool [: the carrier of (() | c11), the carrier of (() | (y9 \ {Cy})):] is non empty set
fC9 is Relation-like the carrier of (() | c11) -defined the carrier of (() | (y9 \ {Cy})) -valued Function-like quasi_total Element of bool [: the carrier of (() | c11), the carrier of (() | (y9 \ {Cy})):]
fC9 . C is set
s2 is non empty TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y
the carrier of s2 is non empty set
U2 is non empty TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y
the carrier of U2 is non empty set
[: the carrier of (() | p2), the carrier of s2:] is non empty set
bool [: the carrier of (() | p2), the carrier of s2:] is non empty set
ty9 is Relation-like the carrier of (() | p2) -defined the carrier of s2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of (() | p2), the carrier of s2:]
[#] (() | c11) is non empty non proper open closed V143() V144() V145() Element of bool the carrier of (() | c11)
bool the carrier of (() | c11) is non empty set
[#] (() | p2) is non empty non proper open closed V143() V144() V145() Element of bool the carrier of (() | p2)
bool the carrier of (() | p2) is non empty set
F2 is non empty V143() V144() V145() Element of bool the carrier of ()
[.(1 / 2),1.[ is V143() V144() V145() non right_end interval Element of bool REAL
c20 is non empty TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y
the carrier of c20 is non empty set
[: the carrier of (() | c11), the carrier of s2:] is non empty set
bool [: the carrier of (() | c11), the carrier of s2:] is non empty set
rng B is Element of bool the carrier of (() | (Y \ {Cy}))
bool the carrier of (() | (Y \ {Cy})) is non empty set
[#] (() | (Y \ {Cy})) is non proper open closed Element of bool the carrier of (() | (Y \ {Cy}))
rng fC9 is Element of bool the carrier of (() | (y9 \ {Cy}))
bool the carrier of (() | (y9 \ {Cy})) is non empty set
[#] (() | (y9 \ {Cy})) is non proper open closed Element of bool the carrier of (() | (y9 \ {Cy}))
sx9 is Relation-like the carrier of (() | c11) -defined the carrier of s2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of (() | c11), the carrier of s2:]
rng sx9 is Element of bool the carrier of s2
bool the carrier of s2 is non empty set
rng ty9 is Element of bool the carrier of s2
(rng sx9) /\ (rng ty9) is Element of bool the carrier of s2
(y9 \ {Cy}) /\ Y is Element of bool the carrier of ()
((y9 \ {Cy}) /\ Y) \ {Cy} is Element of bool the carrier of ()
(y9 /\ Y) \ {Cy} is Element of bool the carrier of ()
((y9 /\ Y) \ {Cy}) \ {Cy} is Element of bool the carrier of ()
{Cy} \/ {Cy} is non empty closed Element of bool the carrier of ()
(y9 /\ Y) \ ({Cy} \/ {Cy}) is Element of bool the carrier of ()
sx9 . C is set
{(sx9 . C)} is non empty trivial set
F1 is non empty V143() V144() V145() Element of bool the carrier of ()
].0,(1 / 2).] is V143() V144() V145() non left_end interval Element of bool REAL
([#] (() | c11)) \/ ([#] (() | p2)) is non empty V143() V144() V145() set
[#] () is non empty non proper open closed V143() V144() V145() Element of bool the carrier of ()
([#] (() | c11)) /\ ([#] (() | p2)) is V143() V144() V145() Element of bool the carrier of (() | p2)
{(1 / 2)} is non empty trivial V143() V144() V145() Element of bool REAL
F is set
fC9 . F is set
B . F is set
[: the carrier of (), the carrier of s2:] is non empty set
bool [: the carrier of (), the carrier of s2:] is non empty set

F is Relation-like the carrier of () -defined the carrier of s2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of (), the carrier of s2:]
[#] U2 is non empty non proper open closed Element of bool the carrier of U2
bool the carrier of U2 is non empty set
[: the carrier of U2, the carrier of ():] is non empty set
bool [: the carrier of U2, the carrier of ():] is non empty set
B /" is Relation-like the carrier of (() | (Y \ {Cy})) -defined the carrier of (() | p2) -valued Function-like total quasi_total Element of bool [: the carrier of (() | (Y \ {Cy})), the carrier of (() | p2):]
[: the carrier of (() | (Y \ {Cy})), the carrier of (() | p2):] is set
bool [: the carrier of (() | (Y \ {Cy})), the carrier of (() | p2):] is non empty set
[: the carrier of c20, the carrier of ():] is non empty set
bool [: the carrier of c20, the carrier of ():] is non empty set
fC9 /" is Relation-like the carrier of (() | (y9 \ {Cy})) -defined the carrier of (() | c11) -valued Function-like total quasi_total Element of bool [: the carrier of (() | (y9 \ {Cy})), the carrier of (() | c11):]
[: the carrier of (() | (y9 \ {Cy})), the carrier of (() | c11):] is set
bool [: the carrier of (() | (y9 \ {Cy})), the carrier of (() | c11):] is non empty set
dom ty9 is V143() V144() V145() Element of bool the carrier of (() | p2)
[#] c20 is non empty non proper open closed Element of bool the carrier of c20
bool the carrier of c20 is non empty set
dom F is V143() V144() V145() Element of bool the carrier of ()
V2 is Element of bool the carrier of s2
r is Element of bool the carrier of ()
{p1} is non empty trivial closed compact bounded Element of bool the carrier of ()
Y /\ (y9 \ {Cy}) is Element of bool the carrier of ()
Y /\ y9 is Element of bool the carrier of ()
(Y /\ y9) \ {Cy} is Element of bool the carrier of ()
[#] s2 is non empty non proper open closed Element of bool the carrier of s2
r /\ ([#] s2) is Element of bool the carrier of s2
r /\ ((y9 \ {Cy}) \/ (Y \ {Cy})) is Element of bool the carrier of ()
Y /\ (Y \ {Cy}) is Element of bool the carrier of ()
(Y /\ (y9 \ {Cy})) \/ (Y /\ (Y \ {Cy})) is Element of bool the carrier of ()
(Y /\ (y9 \ {Cy})) \/ (Y \ {Cy}) is Element of bool the carrier of ()
V1 is Element of bool the carrier of s2
r is Element of bool the carrier of ()
{p1} is non empty trivial closed compact bounded Element of bool the carrier of ()
y9 /\ (Y \ {Cy}) is Element of bool the carrier of ()
[#] s2 is non empty non proper open closed Element of bool the carrier of s2
r /\ ([#] s2) is Element of bool the carrier of s2
r /\ ((y9 \ {Cy}) \/ (Y \ {Cy})) is Element of bool the carrier of ()
y9 /\ (y9 \ {Cy}) is Element of bool the carrier of ()
(y9 /\ (y9 \ {Cy})) \/ (y9 /\ (Y \ {Cy})) is Element of bool the carrier of ()
(y9 \ {Cy}) \/ (y9 /\ (Y \ {Cy})) is Element of bool the carrier of ()
g is Relation-like the carrier of U2 -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [: the carrier of U2, the carrier of ():]
f is Relation-like the carrier of c20 -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [: the carrier of c20, the carrier of ():]

dom sx9 is V143() V144() V145() Element of bool the carrier of (() | c11)
(dom sx9) /\ (dom ty9) is V143() V144() V145() Element of bool the carrier of (() | p2)
{C} is non empty trivial V143() V144() V145() Element of bool REAL
r is set
dom sx9 is set
dom ty9 is set
(dom sx9) /\ (dom ty9) is set
sx9 . r is set
ty9 . r is set
rng F is Element of bool the carrier of s2
(rng sx9) \/ (rng ty9) is Element of bool the carrier of s2
[#] s2 is non empty non proper open closed Element of bool the carrier of s2

([#] c20) /\ ([#] U2) is Element of bool the carrier of U2
r is set
f . r is set
g . r is set
dom B is V143() V144() V145() Element of bool the carrier of (() | p2)
dom fC9 is V143() V144() V145() Element of bool the carrier of (() | c11)
f . p1 is set
([#] c20) \/ ([#] U2) is non empty set
[: the carrier of s2, the carrier of ():] is non empty set
bool [: the carrier of s2, the carrier of ():] is non empty set

F /" is Relation-like the carrier of s2 -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [: the carrier of s2, the carrier of ():]

(fC9 /") +* (B /") is Relation-like Function-like set
r is Relation-like the carrier of s2 -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [: the carrier of s2, the carrier of ():]
D is non empty non trivial closed