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
[:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] 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 [:REAL,REAL:] is non empty set
TOP-REAL 2 is non empty non trivial TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL 2) is functional non empty non trivial set
bool the carrier of (TOP-REAL 2) is non empty set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 compact V197() TopStruct
the carrier of I[01] is non empty V143() V144() V145() set
K199() is V85() V197() L7()
R^1 is non empty strict TopSpace-like T_0 T_1 T_2 V197() TopStruct
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
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (0,1)) is non empty V143() V144() V145() set
ExtREAL is V144() interval set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is set
bool [:COMPLEX,REAL:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is non empty set
{} is empty trivial V143() V144() V145() V146() V147() V148() V149() bounded_below interval 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
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 compact V197() SubSpace of R^1
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 (Closed-Interval-TSpace (0,1))
(0,1) (#) is V72() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
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]
R^2-unit_square is non empty closed connected compact bounded being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | R^2-unit_square is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | R^2-unit_square) is non empty set
D is non empty closed connected compact bounded being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)
C is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
x is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
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
D is Relation-like Function-like set
C is Relation-like Function-like 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
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
D is Relation-like Function-like set
C is Relation-like Function-like 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
D " is Relation-like Function-like set
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
TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL D) is functional non empty set
bool the carrier of (TOP-REAL D) is non empty set
C is Element of bool the carrier of (TOP-REAL D)
x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
y is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
{x} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL D)
C \ {x} is Element of bool the carrier of (TOP-REAL D)
{x,y} is non empty Element of bool the carrier of (TOP-REAL D)
C \ {x,y} is Element of bool the carrier of (TOP-REAL D)
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) /\ ([#] I[01]) is V143() V144() V145() Element of bool the carrier of I[01]
[.C,x.] /\ ([#] I[01]) 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) /\ ([#] I[01]) is V143() V144() V145() Element of bool the carrier of I[01]
[.C,x.] /\ ([#] I[01]) 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) /\ ([#] I[01]) is V143() V144() V145() Element of bool the carrier of I[01]
[.C,x.] /\ ([#] I[01]) 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 (Closed-Interval-TSpace (0,1)) is non empty set
the carrier of (Closed-Interval-TSpace (D,C)) is non empty V143() V144() V145() set
y is V143() V144() V145() Element of bool the carrier of (Closed-Interval-TSpace (0,1))
{} I[01] is empty trivial proper open closed connected compact V143() V144() V145() V146() V147() V148() V149() bounded_below interval Element of bool the carrier of I[01]
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]
I[01] | y is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace 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
lower_bound C is V72() real ext-real Element of REAL
upper_bound C is V72() real ext-real Element of 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 /\ ([#] I[01]) 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
lower_bound D is V72() real ext-real Element of REAL
upper_bound D is V72() real ext-real Element of 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
lower_bound C is V72() real ext-real Element of REAL
upper_bound C is V72() real ext-real Element of REAL
[.(lower_bound C),(upper_bound C).] 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
lower_bound C is V72() real ext-real Element of REAL
upper_bound C is V72() real ext-real Element of REAL
[.(lower_bound C),(upper_bound C).] 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
lower_bound C is V72() real ext-real Element of REAL
upper_bound C is V72() real ext-real Element of REAL
[.(lower_bound C),(upper_bound C).] 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]
I[01] | D is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]
the carrier of (I[01] | D) is V143() V144() V145() set
D is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]
the carrier of D is V143() V144() V145() set
C is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]
the carrier of C is V143() V144() V145() set
() is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]
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]
I[01] | D is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace 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 (TOP-REAL 2)
(TOP-REAL 2) | D is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | D) is non empty set
[: the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | D):] is non empty set
bool [: the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | D):] is non empty set
C is Relation-like the carrier of ((TOP-REAL 2) | R^2-unit_square) -defined the carrier of ((TOP-REAL 2) | D) -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL 2) | R^2-unit_square), the carrier of ((TOP-REAL 2) | D):]
C is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
TOP-REAL C is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is functional non empty set
bool the carrier of (TOP-REAL C) is non empty set
x is non empty Element of bool the carrier of (TOP-REAL C)
y is V35(C) V77() V135() Element of the carrier of (TOP-REAL C)
y9 is V35(C) V77() V135() Element of the carrier of (TOP-REAL C)
{y,y9} is non empty Element of bool the carrier of (TOP-REAL C)
x \ {y,y9} is Element of bool the carrier of (TOP-REAL C)
(TOP-REAL C) | (x \ {y,y9}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C
(TOP-REAL C) | x is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C
the carrier of ((TOP-REAL C) | x) is non empty set
[: the carrier of I[01], the carrier of ((TOP-REAL C) | x):] is non empty set
bool [: the carrier of I[01], the carrier of ((TOP-REAL C) | x):] is non empty set
Y is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL C) | x) -valued Function-like non empty total quasi_total Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL C) | x):]
Y . 0 is set
Y . 1 is set
rng Y is Element of bool the carrier of ((TOP-REAL C) | x)
bool the carrier of ((TOP-REAL C) | x) is non empty set
[#] ((TOP-REAL C) | x) is non empty non proper open closed Element of bool the carrier of ((TOP-REAL C) | 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 ((TOP-REAL C) | x)
Y .: the carrier of I[01] is Element of bool the carrier of ((TOP-REAL C) | x)
Y .: {0,1} is Element of bool the carrier of ((TOP-REAL C) | x)
(Y .: the carrier of I[01]) \ (Y .: {0,1}) is Element of bool the carrier of ((TOP-REAL C) | x)
x \ (Y .: {0,1}) is Element of bool the carrier of (TOP-REAL C)
p1 is non empty Element of bool the carrier of (TOP-REAL C)
(TOP-REAL C) | 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 ((TOP-REAL C) | x)
((TOP-REAL C) | x) | Cy is strict TopSpace-like T_0 T_1 T_2 SubSpace of (TOP-REAL C) | x
Y /" is Relation-like the carrier of ((TOP-REAL C) | x) -defined the carrier of I[01] -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL C) | x), the carrier of I[01]:]
[: the carrier of ((TOP-REAL C) | x), the carrier of I[01]:] is non empty set
bool [: the carrier of ((TOP-REAL C) | x), the carrier of I[01]:] is non empty set
(Y /") | p1 is Relation-like the carrier of ((TOP-REAL C) | x) -defined the carrier of I[01] -valued Function-like Element of bool [: the carrier of ((TOP-REAL C) | x), the carrier of I[01]:]
the carrier of ((TOP-REAL C) | p1) is non empty set
[: the carrier of ((TOP-REAL C) | p1), the carrier of I[01]:] is non empty set
bool [: the carrier of ((TOP-REAL C) | p1), the carrier of I[01]:] is non empty set
B is Relation-like the carrier of ((TOP-REAL C) | p1) -defined the carrier of I[01] -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL C) | p1), the carrier of I[01]:]
Y | the carrier of () is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL C) | x) -valued Function-like Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL C) | x):]
D is V143() V144() V145() Element of bool the carrier of I[01]
I[01] | D is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]
the carrier of (I[01] | D) is V143() V144() V145() set
[: the carrier of (I[01] | D), the carrier of ((TOP-REAL C) | x):] is set
bool [: the carrier of (I[01] | D), the carrier of ((TOP-REAL C) | x):] is non empty set
dom (Y | the carrier of ()) is V143() V144() V145() Element of bool the carrier of I[01]
Y " is Relation-like Function-like set
rng (Y | the carrier of ()) is Element of bool the carrier of ((TOP-REAL C) | x)
the carrier of ((TOP-REAL C) | (x \ {y,y9})) is set
[: the carrier of (), the carrier of ((TOP-REAL C) | (x \ {y,y9})):] is set
bool [: the carrier of (), the carrier of ((TOP-REAL C) | (x \ {y,y9})):] is non empty set
fC9 is Relation-like the carrier of () -defined the carrier of ((TOP-REAL C) | (x \ {y,y9})) -valued Function-like quasi_total Element of bool [: the carrier of (), the carrier of ((TOP-REAL C) | (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 ((TOP-REAL C) | (x \ {y,y9})) -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of ((TOP-REAL C) | (x \ {y,y9})), the carrier of ():]
[: the carrier of ((TOP-REAL C) | (x \ {y,y9})), the carrier of ():] is set
bool [: the carrier of ((TOP-REAL C) | (x \ {y,y9})), the carrier of ():] is non empty set
fC9 " is Relation-like Function-like set
fC9 is Relation-like the carrier of (I[01] | D) -defined the carrier of ((TOP-REAL C) | x) -valued Function-like total quasi_total Element of bool [: the carrier of (I[01] | D), the carrier of ((TOP-REAL C) | x):]
rng fC9 is Element of bool the carrier of ((TOP-REAL C) | (x \ {y,y9}))
bool the carrier of ((TOP-REAL C) | (x \ {y,y9})) is non empty set
[#] ((TOP-REAL C) | (x \ {y,y9})) is non proper open closed Element of bool the carrier of ((TOP-REAL C) | (x \ {y,y9}))
D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL D) is functional non empty set
bool the carrier of (TOP-REAL D) is non empty set
C is Element of bool the carrier of (TOP-REAL D)
(TOP-REAL D) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
y is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
the carrier of ((TOP-REAL D) | C) is set
[: the carrier of I[01], the carrier of ((TOP-REAL D) | C):] is set
bool [: the carrier of I[01], the carrier of ((TOP-REAL D) | C):] is non empty set
y9 is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL D) | C) -valued Function-like quasi_total Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL D) | 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
TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL D) is functional non empty set
C is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
LSeg (C,x) is Element of bool the carrier of (TOP-REAL D)
bool the carrier of (TOP-REAL D) is non empty set
(TOP-REAL D) | (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
y is TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]
the carrier of y is V143() V144() V145() set
y9 is TopSpace-like T_0 T_1 T_2 V197() SubSpace of I[01]
(#) (C,x) is V72() real ext-real Element of the carrier of (Closed-Interval-TSpace (C,x))
the carrier of (Closed-Interval-TSpace (C,x)) is non empty V143() V144() V145() set
(C,x) (#) is V72() real ext-real Element of the carrier of (Closed-Interval-TSpace (C,x))
L[01] (((#) (C,x)),((C,x) (#))) is Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (C,x)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (C,x)):]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (C,x)):] is non empty set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (C,x)):] is non empty set
D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL D) is functional non empty set
bool the carrier of (TOP-REAL D) is non empty set
C is Element of bool the carrier of (TOP-REAL D)
(TOP-REAL D) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of ((TOP-REAL D) | C) is set
x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
y is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
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 (Closed-Interval-TSpace (0,1)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (y9,Y)), the carrier of (Closed-Interval-TSpace (0,1)):]
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 (Closed-Interval-TSpace (0,1)):] is non empty set
bool [: the carrier of (Closed-Interval-TSpace (y9,Y)), the carrier of (Closed-Interval-TSpace (0,1)):] is non empty set
[: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | C):] is set
bool [: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | 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 (TOP-REAL D)
(TOP-REAL D) | p2 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of ((TOP-REAL D) | p2) is non empty set
[: the carrier of I[01], the carrier of ((TOP-REAL D) | p2):] is non empty set
bool [: the carrier of I[01], the carrier of ((TOP-REAL D) | p2):] is non empty set
B is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL D) | p2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL D) | 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 ((TOP-REAL D) | p2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | p2):]
[: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | p2):] is non empty set
bool [: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | p2):] is non empty set
fC9 is Relation-like the carrier of (I[01] | Cy) -defined the carrier of ((TOP-REAL D) | C) -valued Function-like quasi_total Element of bool [: the carrier of (I[01] | Cy), the carrier of ((TOP-REAL D) | 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
D is TopSpace-like TopStruct
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:]
y is TopSpace-like TopStruct
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
TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL D) is functional non empty set
bool the carrier of (TOP-REAL D) is non empty set
C is Element of bool the carrier of (TOP-REAL D)
x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
y is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
{x} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL D)
C \ {x} is Element of bool the carrier of (TOP-REAL D)
(TOP-REAL D) | (C \ {x}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of ((TOP-REAL D) | (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 (TOP-REAL D)
(TOP-REAL D) | Cy is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of ((TOP-REAL D) | 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 ((TOP-REAL D) | Cy):] is non empty set
bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):] is non empty set
p2 is Relation-like the carrier of (I[01] | p1) -defined the carrier of ((TOP-REAL D) | Cy) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | 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 ((TOP-REAL D) | Cy) -valued Function-like Element of bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):]
p2 /" is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):]
[: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):] is non empty set
bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):] is non empty set
(TOP-REAL D) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of ((TOP-REAL D) | C) is set
bool the carrier of ((TOP-REAL D) | 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 ((TOP-REAL D) | C)
((TOP-REAL D) | C) | fC9 is strict TopSpace-like T_0 T_1 T_2 SubSpace of (TOP-REAL D) | 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 ((TOP-REAL D) | Cy)
bool the carrier of ((TOP-REAL D) | Cy) is non empty set
[#] ((TOP-REAL D) | C) is non proper open closed Element of bool the carrier of ((TOP-REAL D) | 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 ((TOP-REAL D) | Cy)
p2 .: p1 is Element of bool the carrier of ((TOP-REAL D) | 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 ((TOP-REAL D) | Cy)
{(p2 . y9)} is non empty trivial set
(p2 .: p1) \ {(p2 . y9)} is Element of bool the carrier of ((TOP-REAL D) | Cy)
(rng p2) \ {x} is Element of bool the carrier of ((TOP-REAL D) | Cy)
[#] ((TOP-REAL D) | (C \ {x})) is non proper open closed Element of bool the carrier of ((TOP-REAL D) | (C \ {x}))
bool the carrier of ((TOP-REAL D) | (C \ {x})) is non empty set
rng (p2 | B) is Element of bool the carrier of ((TOP-REAL D) | Cy)
[: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {x})):] is set
bool [: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {x})):] is non empty set
p2 is Relation-like the carrier of (() | B) -defined the carrier of ((TOP-REAL D) | (C \ {x})) -valued Function-like quasi_total Element of bool [: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {x})):]
p2 . Y is set
p2 /" is Relation-like the carrier of ((TOP-REAL D) | (C \ {x})) -defined the carrier of (() | B) -valued Function-like total quasi_total Element of bool [: the carrier of ((TOP-REAL D) | (C \ {x})), the carrier of (() | B):]
[: the carrier of ((TOP-REAL D) | (C \ {x})), the carrier of (() | B):] is set
bool [: the carrier of ((TOP-REAL D) | (C \ {x})), the carrier of (() | B):] is non empty set
p2 " is Relation-like Function-like set
p2 " is Relation-like Function-like set
(p2 ") | (p2 .: B) is Relation-like set
(p2 /") | ([#] ((TOP-REAL D) | (C \ {x}))) is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):]
(p2 /") | fC9 is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of ((TOP-REAL D) | 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
TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL D) is functional non empty set
bool the carrier of (TOP-REAL D) is non empty set
C is Element of bool the carrier of (TOP-REAL D)
x is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
y is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
{y} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL D)
C \ {y} is Element of bool the carrier of (TOP-REAL D)
(TOP-REAL D) | (C \ {y}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of ((TOP-REAL D) | (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 (TOP-REAL D)
(TOP-REAL D) | Cy is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of ((TOP-REAL D) | 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 ((TOP-REAL D) | Cy):] is non empty set
bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):] is non empty set
p2 is Relation-like the carrier of (I[01] | p1) -defined the carrier of ((TOP-REAL D) | Cy) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | 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 ((TOP-REAL D) | Cy) -valued Function-like Element of bool [: the carrier of (I[01] | p1), the carrier of ((TOP-REAL D) | Cy):]
p2 /" is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):]
[: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):] is non empty set
bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):] is non empty set
(TOP-REAL D) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
the carrier of ((TOP-REAL D) | C) is set
bool the carrier of ((TOP-REAL D) | 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 ((TOP-REAL D) | C)
((TOP-REAL D) | C) | fC9 is strict TopSpace-like T_0 T_1 T_2 SubSpace of (TOP-REAL D) | 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 ((TOP-REAL D) | Cy)
bool the carrier of ((TOP-REAL D) | Cy) is non empty set
[#] ((TOP-REAL D) | C) is non proper open closed Element of bool the carrier of ((TOP-REAL D) | 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 ((TOP-REAL D) | Cy)
p2 .: p1 is Element of bool the carrier of ((TOP-REAL D) | 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 ((TOP-REAL D) | Cy)
{(p2 . Y)} is non empty trivial set
(p2 .: p1) \ {(p2 . Y)} is Element of bool the carrier of ((TOP-REAL D) | Cy)
(rng p2) \ {y} is Element of bool the carrier of ((TOP-REAL D) | Cy)
[#] ((TOP-REAL D) | (C \ {y})) is non proper open closed Element of bool the carrier of ((TOP-REAL D) | (C \ {y}))
bool the carrier of ((TOP-REAL D) | (C \ {y})) is non empty set
rng (p2 | B) is Element of bool the carrier of ((TOP-REAL D) | Cy)
[: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {y})):] is set
bool [: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {y})):] is non empty set
p2 is Relation-like the carrier of (() | B) -defined the carrier of ((TOP-REAL D) | (C \ {y})) -valued Function-like quasi_total Element of bool [: the carrier of (() | B), the carrier of ((TOP-REAL D) | (C \ {y})):]
p2 . y9 is set
p2 /" is Relation-like the carrier of ((TOP-REAL D) | (C \ {y})) -defined the carrier of (() | B) -valued Function-like total quasi_total Element of bool [: the carrier of ((TOP-REAL D) | (C \ {y})), the carrier of (() | B):]
[: the carrier of ((TOP-REAL D) | (C \ {y})), the carrier of (() | B):] is set
bool [: the carrier of ((TOP-REAL D) | (C \ {y})), the carrier of (() | B):] is non empty set
p2 " is Relation-like Function-like set
p2 " is Relation-like Function-like set
(p2 ") | (p2 .: B) is Relation-like set
(p2 /") | ([#] ((TOP-REAL D) | (C \ {y}))) is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of ((TOP-REAL D) | Cy), the carrier of (I[01] | p1):]
(p2 /") | fC9 is Relation-like the carrier of ((TOP-REAL D) | Cy) -defined the carrier of (I[01] | p1) -valued Function-like Element of bool [: the carrier of ((TOP-REAL D) | 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
TOP-REAL y is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL y) is functional non empty set
bool the carrier of (TOP-REAL y) is non empty set
y9 is Element of bool the carrier of (TOP-REAL y)
Y is Element of bool the carrier of (TOP-REAL y)
y9 /\ Y is Element of bool the carrier of (TOP-REAL y)
Cy is V35(y) V77() V135() Element of the carrier of (TOP-REAL y)
p1 is V35(y) V77() V135() Element of the carrier of (TOP-REAL y)
{Cy,p1} is non empty Element of bool the carrier of (TOP-REAL y)
{Cy} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL y)
y9 \ {Cy} is Element of bool the carrier of (TOP-REAL y)
Y \ {Cy} is Element of bool the carrier of (TOP-REAL y)
(y9 \ {Cy}) \/ (Y \ {Cy}) is Element of bool the carrier of (TOP-REAL y)
(TOP-REAL y) | ((y9 \ {Cy}) \/ (Y \ {Cy})) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y
(TOP-REAL y) | (Y \ {Cy}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y
the carrier of ((TOP-REAL y) | (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 ((TOP-REAL y) | (Y \ {Cy})):] is set
bool [: the carrier of (() | p2), the carrier of ((TOP-REAL y) | (Y \ {Cy})):] is non empty set
B is Relation-like the carrier of (() | p2) -defined the carrier of ((TOP-REAL y) | (Y \ {Cy})) -valued Function-like quasi_total Element of bool [: the carrier of (() | p2), the carrier of ((TOP-REAL y) | (Y \ {Cy})):]
B . C is set
(TOP-REAL y) | (y9 \ {Cy}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL y
the carrier of ((TOP-REAL y) | (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 ((TOP-REAL y) | (y9 \ {Cy})):] is set
bool [: the carrier of (() | c11), the carrier of ((TOP-REAL y) | (y9 \ {Cy})):] is non empty set
fC9 is Relation-like the carrier of (() | c11) -defined the carrier of ((TOP-REAL y) | (y9 \ {Cy})) -valued Function-like quasi_total Element of bool [: the carrier of (() | c11), the carrier of ((TOP-REAL y) | (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 ((TOP-REAL y) | (Y \ {Cy}))
bool the carrier of ((TOP-REAL y) | (Y \ {Cy})) is non empty set
[#] ((TOP-REAL y) | (Y \ {Cy})) is non proper open closed Element of bool the carrier of ((TOP-REAL y) | (Y \ {Cy}))
rng fC9 is Element of bool the carrier of ((TOP-REAL y) | (y9 \ {Cy}))
bool the carrier of ((TOP-REAL y) | (y9 \ {Cy})) is non empty set
[#] ((TOP-REAL y) | (y9 \ {Cy})) is non proper open closed Element of bool the carrier of ((TOP-REAL y) | (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 (TOP-REAL y)
((y9 \ {Cy}) /\ Y) \ {Cy} is Element of bool the carrier of (TOP-REAL y)
(y9 /\ Y) \ {Cy} is Element of bool the carrier of (TOP-REAL y)
((y9 /\ Y) \ {Cy}) \ {Cy} is Element of bool the carrier of (TOP-REAL y)
{Cy} \/ {Cy} is non empty closed Element of bool the carrier of (TOP-REAL y)
(y9 /\ Y) \ ({Cy} \/ {Cy}) is Element of bool the carrier of (TOP-REAL y)
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
sx9 +* B is Relation-like Function-like 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 ((TOP-REAL y) | (Y \ {Cy})) -defined the carrier of (() | p2) -valued Function-like total quasi_total Element of bool [: the carrier of ((TOP-REAL y) | (Y \ {Cy})), the carrier of (() | p2):]
[: the carrier of ((TOP-REAL y) | (Y \ {Cy})), the carrier of (() | p2):] is set
bool [: the carrier of ((TOP-REAL y) | (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 ((TOP-REAL y) | (y9 \ {Cy})) -defined the carrier of (() | c11) -valued Function-like total quasi_total Element of bool [: the carrier of ((TOP-REAL y) | (y9 \ {Cy})), the carrier of (() | c11):]
[: the carrier of ((TOP-REAL y) | (y9 \ {Cy})), the carrier of (() | c11):] is set
bool [: the carrier of ((TOP-REAL y) | (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 (TOP-REAL y)
{p1} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL y)
Y /\ (y9 \ {Cy}) is Element of bool the carrier of (TOP-REAL y)
Y /\ y9 is Element of bool the carrier of (TOP-REAL y)
(Y /\ y9) \ {Cy} is Element of bool the carrier of (TOP-REAL y)
[#] 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 (TOP-REAL y)
Y /\ (Y \ {Cy}) is Element of bool the carrier of (TOP-REAL y)
(Y /\ (y9 \ {Cy})) \/ (Y /\ (Y \ {Cy})) is Element of bool the carrier of (TOP-REAL y)
(Y /\ (y9 \ {Cy})) \/ (Y \ {Cy}) is Element of bool the carrier of (TOP-REAL y)
V1 is Element of bool the carrier of s2
r is Element of bool the carrier of (TOP-REAL y)
{p1} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL y)
y9 /\ (Y \ {Cy}) is Element of bool the carrier of (TOP-REAL y)
[#] 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 (TOP-REAL y)
y9 /\ (y9 \ {Cy}) is Element of bool the carrier of (TOP-REAL y)
(y9 /\ (y9 \ {Cy})) \/ (y9 /\ (Y \ {Cy})) is Element of bool the carrier of (TOP-REAL y)
(y9 \ {Cy}) \/ (y9 /\ (Y \ {Cy})) is Element of bool the carrier of (TOP-REAL y)
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 ():]
B " is Relation-like Function-like set
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
fC9 " is Relation-like Function-like set
([#] 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 +* g is Relation-like Function-like 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 ():]
F " is Relation-like Function-like set
(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 connected compact bounded being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)
C is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
{C} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL 2)
D \ {C} is Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (D \ {C}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
x is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
{C,x} is non empty Element of bool the carrier of (TOP-REAL 2)
y9 is non empty Element of bool the carrier of (TOP-REAL 2)
Y is non empty Element of bool the carrier of (TOP-REAL 2)
y9 \/ Y is non empty Element of bool the carrier of (TOP-REAL 2)
y9 /\ Y is Element of bool the carrier of (TOP-REAL 2)
y9 \ {C} is Element of bool the carrier of (TOP-REAL 2)
Y \ {C} is Element of bool the carrier of (TOP-REAL 2)
(y9 \ {C}) \/ (Y \ {C}) is Element of bool the carrier of (TOP-REAL 2)
y is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | y is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
D is non empty non trivial closed connected compact bounded being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)
C is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
x is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
{C} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL 2)
D \ {C} is Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (D \ {C}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
{x} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL 2)
D \ {x} is Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (D \ {x}) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
y9 is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | y9 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
y is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | y is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
D is natural V72() real ext-real V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
TOP-REAL D is non empty TopSpace-like T_0 T_1 T_2 V109() V155() V156() V157() V158() V159() V160() V161() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL D) is functional non empty set
bool the carrier of (TOP-REAL D) is non empty set
C is non empty Element of bool the carrier of (TOP-REAL D)
(TOP-REAL D) | C is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL D
x is V143() V144() V145() Element of bool the carrier of ()
() | x is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of ()
y9 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]
[.y,y9.] is V143() V144() V145() closed interval Element of bool REAL
the carrier of ((TOP-REAL D) | C) is non empty set
[: the carrier of I[01], the carrier of ((TOP-REAL D) | C):] is non empty set
bool [: the carrier of I[01], the carrier of ((TOP-REAL D) | C):] is non empty set
Y is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL D) | C) -valued Function-like non empty total quasi_total Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL D) | C):]
Y . 0 is set
Y . 1 is set
p2 is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
B is V35(D) V77() V135() Element of the carrier of (TOP-REAL D)
D is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | D is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | D) is non empty set
[: the carrier of ((TOP-REAL 2) | D), the carrier of ():] is non empty set
bool [: the carrier of ((TOP-REAL 2) | D), the carrier of ():] is non empty set
C is Relation-like the carrier of ((TOP-REAL 2) | D) -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL 2) | D), the carrier of ():]
x is non empty Element of bool the carrier of (TOP-REAL 2)
C .: x is V143() V144() V145() Element of bool the carrier of ()
bool the carrier of ((TOP-REAL 2) | D) is non empty set
dom C is Element of bool the carrier of ((TOP-REAL 2) | D)
C " (C .: x) is Element of bool the carrier of ((TOP-REAL 2) | D)
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
rng C 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 ()
C /" is Relation-like the carrier of () -defined the carrier of ((TOP-REAL 2) | D) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (), the carrier of ((TOP-REAL 2) | D):]
[: the carrier of (), the carrier of ((TOP-REAL 2) | D):] is non empty set
bool [: the carrier of (), the carrier of ((TOP-REAL 2) | D):] is non empty set
Cy is V143() V144() V145() Element of bool the carrier of ()
(C /") .: Cy is Element of bool the carrier of ((TOP-REAL 2) | D)
(TOP-REAL 2) | x is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | x) is non empty set
(C /") | Cy is Relation-like the carrier of () -defined the carrier of ((TOP-REAL 2) | D) -valued Function-like Element of bool [: the carrier of (), the carrier of ((TOP-REAL 2) | D):]
() | Cy is strict TopSpace-like T_0 T_1 T_2 V197() SubSpace of ()
the carrier of (() | Cy) is V143() V144() V145() set
[: the carrier of (() | Cy), the carrier of ((TOP-REAL 2) | D):] is set
bool [: the carrier of (() | Cy), the carrier of ((TOP-REAL 2) | D):] is non empty set
rng ((C /") | Cy) is Element of bool the carrier of ((TOP-REAL 2) | D)
[#] ((TOP-REAL 2) | x) is non empty non proper open closed Element of bool the carrier of ((TOP-REAL 2) | x)
bool the carrier of ((TOP-REAL 2) | x) is non empty set
[: the carrier of (() | Cy), the carrier of ((TOP-REAL 2) | x):] is set
bool [: the carrier of (() | Cy), the carrier of ((TOP-REAL 2) | x):] is non empty set
p2 is Relation-like the carrier of (() | Cy) -defined the carrier of ((TOP-REAL 2) | x) -valued Function-like total quasi_total Element of bool [: the carrier of (() | Cy), the carrier of ((TOP-REAL 2) | x):]
p2 /" is Relation-like the carrier of ((TOP-REAL 2) | x) -defined the carrier of (() | Cy) -valued Function-like quasi_total Element of bool [: the carrier of ((TOP-REAL 2) | x), the carrier of (() | Cy):]
[: the carrier of ((TOP-REAL 2) | x), the carrier of (() | Cy):] is set
bool [: the carrier of ((TOP-REAL 2) | x), the carrier of (() | Cy):] is non empty set
p2 " is Relation-like Function-like set
(C /") " is Relation-like Function-like set
((C /") ") | ((C /") .: Cy) is Relation-like set
C " is Relation-like Function-like set
(C ") " is Relation-like Function-like set
((C ") ") | ((C /") .: Cy) is Relation-like set
C | x is Relation-like the carrier of ((TOP-REAL 2) | D) -defined the carrier of () -valued Function-like Element of bool [: the carrier of ((TOP-REAL 2) | D), the carrier of ():]
dom (C /") is V143() V144() V145() Element of bool the carrier of ()
dom p2 is V143() V144() V145() Element of bool the carrier of (() | Cy)
bool the carrier of (() | Cy) is non empty set
[#] (() | Cy) is non proper open closed V143() V144() V145() Element of bool the carrier of (() | Cy)
y is Element of bool the carrier of ((TOP-REAL 2) | D)
((TOP-REAL 2) | D) | y is strict TopSpace-like T_0 T_1 T_2 SubSpace of (TOP-REAL 2) | D
B is Relation-like the carrier of ((TOP-REAL 2) | x) -defined the carrier of (() | Cy) -valued Function-like quasi_total Element of bool [: the carrier of ((TOP-REAL 2) | x), the carrier of (() | Cy):]
D is non empty non trivial closed connected compact bounded being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)
C is non empty closed connected compact bounded Element of bool the carrier of (TOP-REAL 2)
x is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
{x} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL 2)
D \ {x} is Element of bool the carrier of (TOP-REAL 2)
y is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
y9 is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
Y is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | Y is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | Y) is non empty set
[: the carrier of ((TOP-REAL 2) | Y), the carrier of ():] is non empty set
bool [: the carrier of ((TOP-REAL 2) | Y), the carrier of ():] is non empty set
Cy is Relation-like the carrier of ((TOP-REAL 2) | Y) -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL 2) | Y), the carrier of ():]
bool the carrier of ((TOP-REAL 2) | Y) is non empty set
[#] ((TOP-REAL 2) | Y) is non empty non proper open closed Element of bool the carrier of ((TOP-REAL 2) | Y)
p1 is Element of bool the carrier of ((TOP-REAL 2) | Y)
Cy .: p1 is V143() V144() V145() Element of bool the carrier of ()
rng Cy 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 ()
B is closed connected compact V143() V144() V145() Element of bool the carrier of ()
c11 is V143() V144() V145() Element of bool the carrier of I[01]
fC9 is V143() V144() V145() Element of bool the carrier of ()
dom Cy is Element of bool the carrier of ((TOP-REAL 2) | Y)
Cy . y9 is set
fC9 is non empty closed connected compact V143() V144() V145() Element of bool the carrier of I[01]
fC9 is V72() real ext-real Element of the carrier of I[01]
p1 is V72() real ext-real Element of the carrier of I[01]
[.fC9,p1.] is V143() V144() V145() closed interval Element of bool REAL
Cy . y is set
{fC9} is non empty trivial V143() V144() V145() Element of bool REAL
D is non empty closed compact V143() V144() V145() Element of bool the carrier of I[01]
lower_bound D is V72() real ext-real set
upper_bound D is V72() real ext-real set
C is V143() V144() V145() Element of bool REAL
lower_bound C is V72() real ext-real Element of REAL
upper_bound C is V72() real ext-real Element of REAL
[.(lower_bound C),(upper_bound C).] is V143() V144() V145() closed interval Element of bool REAL
x is V143() V144() V145() Element of bool REAL
y is set
y9 is V72() real ext-real Element of REAL
lower_bound x is V72() real ext-real Element of REAL
upper_bound x is V72() real ext-real Element of REAL
[.(lower_bound x),(upper_bound x).] is V143() V144() V145() closed interval Element of bool REAL
y is set
y is non empty V143() V144() V145() closed_interval interval Element of bool REAL
lower_bound y is V72() real ext-real Element of REAL
upper_bound y is V72() real ext-real Element of REAL
D is non empty closed compact V143() V144() V145() Element of bool the carrier of I[01]
lower_bound D is V72() real ext-real set
upper_bound D is V72() real ext-real set
C is non empty V143() V144() V145() closed_interval interval Element of bool REAL
lower_bound C is V72() real ext-real Element of REAL
upper_bound C is V72() real ext-real Element of REAL
x is V72() real ext-real Element of REAL
y is V72() real ext-real Element of REAL
[.x,y.] is V143() V144() V145() closed interval Element of bool REAL
y9 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]
[.y9,Y.] is V143() V144() V145() closed interval Element of bool REAL
D is non empty non trivial closed connected compact bounded being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)
C is closed Element of bool the carrier of (TOP-REAL 2)
x is closed compact bounded Element of bool the carrier of (TOP-REAL 2)
y is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
y9 is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
Y is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
{Y} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL 2)
D \ {Y} is Element of bool the carrier of (TOP-REAL 2)
Cy is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | Cy is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | Cy) is non empty set
[: the carrier of ((TOP-REAL 2) | Cy), the carrier of ():] is non empty set
bool [: the carrier of ((TOP-REAL 2) | Cy), the carrier of ():] is non empty set
p1 is Relation-like the carrier of ((TOP-REAL 2) | Cy) -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((TOP-REAL 2) | Cy), the carrier of ():]
dom p1 is Element of bool the carrier of ((TOP-REAL 2) | Cy)
bool the carrier of ((TOP-REAL 2) | Cy) is non empty set
[#] ((TOP-REAL 2) | Cy) is non empty non proper open closed Element of bool the carrier of ((TOP-REAL 2) | Cy)
p2 is Element of bool the carrier of ((TOP-REAL 2) | Cy)
p1 .: p2 is V143() V144() V145() Element of bool the carrier of ()
rng p1 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 ()
c11 is closed compact V143() V144() V145() Element of bool the carrier of ()
fC9 is V143() V144() V145() Element of bool the carrier of I[01]
fC9 is V143() V144() V145() Element of bool the carrier of ()
p1 . y9 is set
fC9 is non empty closed compact V143() V144() V145() Element of bool the carrier of I[01]
p1 is V72() real ext-real Element of the carrier of I[01]
p2 is V72() real ext-real Element of the carrier of I[01]
[.p1,p2.] is V143() V144() V145() closed interval Element of bool REAL
E is non empty closed connected compact V143() V144() V145() Element of bool the carrier of I[01]
p1 " E is Element of bool the carrier of ((TOP-REAL 2) | Cy)
p1 . y is set
{p1} is non empty trivial V143() V144() V145() Element of bool REAL
p1 .: (p1 " E) is V143() V144() V145() Element of bool the carrier of ()
B is non empty Element of bool the carrier of (TOP-REAL 2)
s1 is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
s2 is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
x is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
y is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
{x,y} is non empty Element of bool the carrier of (TOP-REAL 2)
y9 is Element of bool the carrier of (TOP-REAL 2)
{x} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL 2)
{y} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL 2)
Y is Element of bool the carrier of (TOP-REAL 2)
Cy is Element of bool the carrier of (TOP-REAL 2)
Y \/ Cy is Element of bool the carrier of (TOP-REAL 2)
D \ y9 is Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | D is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
{} ((TOP-REAL 2) | D) is empty trivial proper open closed connected compact V143() V144() V145() V146() V147() V148() V149() bounded_below interval Element of bool the carrier of ((TOP-REAL 2) | D)
the carrier of ((TOP-REAL 2) | D) is non empty set
bool the carrier of ((TOP-REAL 2) | D) is non empty set
p1 is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
p2 is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
B is Element of bool the carrier of (TOP-REAL 2)
x is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
{x} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL 2)
y is Element of D
y9 is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
{y9} is non empty trivial closed compact bounded Element of bool the carrier of (TOP-REAL 2)
Y is non empty closed compact bounded Element of bool the carrier of (TOP-REAL 2)
C \/ Y is non empty closed Element of bool the carrier of (TOP-REAL 2)
Cy is non empty closed compact bounded Element of bool the carrier of (TOP-REAL 2)
D \ Cy is Element of bool the carrier of (TOP-REAL 2)
{x,y} is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | D is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
{} ((TOP-REAL 2) | D) is empty trivial proper open closed connected compact V143() V144() V145() V146() V147() V148() V149() bounded_below interval Element of bool the carrier of ((TOP-REAL 2) | D)
the carrier of ((TOP-REAL 2) | D) is non empty set
bool the carrier of ((TOP-REAL 2) | D) is non empty set
{y} is non empty trivial Element of bool D
bool D is non empty set
p1 is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
p2 is V35(2) V77() V135() Element of the carrier of (TOP-REAL 2)
B is Element of bool the carrier of (TOP-REAL 2)