REAL is non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval set
NAT is V166() V167() V168() V169() V170() V171() V172() V200() bounded_below Element of bool REAL
bool REAL is non empty set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact SubSpace of R^1
R^1 is non empty strict TopSpace-like T_0 T_1 T_2 V211() TopStruct
the carrier of I[01] is non empty V166() V167() V168() set
[:I[01],I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of [:I[01],I[01]:] is non empty set
COMPLEX is non empty V42() V166() V172() set
omega is V166() V167() V168() V169() V170() V171() V172() V200() bounded_below set
bool omega is non empty set
bool NAT is non empty set
1 is non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below Element of NAT
RAT is non empty V42() V166() V167() V168() V169() V172() set
[:1,1:] is Relation-like RAT -valued INT -valued non empty V156() V157() V158() V159() set
INT is non empty V42() V166() V167() V168() V169() V170() V172() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is Relation-like RAT -valued INT -valued non empty V156() V157() V158() V159() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is Relation-like non empty V156() V157() V158() set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is Relation-like non empty V156() V157() V158() set
[:[:REAL,REAL:],REAL:] is Relation-like non empty V156() V157() V158() set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below Element of NAT
[:2,2:] is Relation-like RAT -valued INT -valued non empty V156() V157() V158() V159() set
[:[:2,2:],REAL:] is Relation-like non empty V156() V157() V158() set
bool [:[:2,2:],REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected RLTopStruct
the carrier of (TOP-REAL 2) is functional non empty 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 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact TopStruct
the carrier of I[01] is non empty V166() V167() V168() set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V211() MetrStruct
0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval Element of NAT
the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval set
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like T_0 T_1 T_2 V211() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (0,1)) is non empty V166() V167() V168() set
[:R^1,R^1:] is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of [:R^1,R^1:] is non empty set
[: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):] is Relation-like non empty set
bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):] is non empty set
{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval set
{{},1} is non empty set
K618() is non empty strict TopSpace-like T_0 T_1 T_2 V211() V271() SubSpace of R^1
the carrier of K618() is non empty V166() V167() V168() set
bool the carrier of K618() is non empty set
bool (bool the carrier of K618()) is non empty set
Tunit_circle 2 is non empty TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact V246() being_simple_closed_curve pathwise_connected pseudocompact SubSpace of TOP-REAL 2
the carrier of (Tunit_circle 2) is non empty set
[: the carrier of K618(), the carrier of (Tunit_circle 2):] is Relation-like non empty set
bool [: the carrier of K618(), the carrier of (Tunit_circle 2):] is non empty set
CircleMap is Relation-like the carrier of K618() -defined the carrier of K618() -defined the carrier of (Tunit_circle 2) -valued the carrier of (Tunit_circle 2) -valued Function-like non empty total total quasi_total quasi_total onto continuous Element of bool [: the carrier of K618(), the carrier of (Tunit_circle 2):]
c[10] is Element of the carrier of (Tunit_circle 2)
Topen_unit_circle c[10] is non empty strict TopSpace-like T_0 T_1 T_2 V118( Tunit_circle 2) SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[10]) is non empty set
].0,1.[ is non empty V166() V167() V168() non left_end non right_end bounded_below bounded_above real-bounded interval Element of bool REAL
R^1 ].0,1.[ is non empty connected V166() V167() V168() interval Element of bool the carrier of K618()
K618() | (R^1 ].0,1.[) is non empty strict TopSpace-like T_0 T_1 T_2 V211() V271() SubSpace of K618()
the carrier of (K618() | (R^1 ].0,1.[)) is non empty V166() V167() V168() set
[: the carrier of (Topen_unit_circle c[10]), the carrier of (K618() | (R^1 ].0,1.[)):] is Relation-like non empty V156() V157() V158() set
bool [: the carrier of (Topen_unit_circle c[10]), the carrier of (K618() | (R^1 ].0,1.[)):] is non empty set
c[-10] is Element of the carrier of (Tunit_circle 2)
Topen_unit_circle c[-10] is non empty strict TopSpace-like T_0 T_1 T_2 V118( Tunit_circle 2) SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[-10]) is non empty set
1 / 2 is complex ext-real non negative real Element of REAL
3 is non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below Element of NAT
3 / 2 is complex ext-real non negative real Element of REAL
].(1 / 2),(3 / 2).[ is non empty V166() V167() V168() non left_end non right_end bounded_below bounded_above real-bounded interval Element of bool REAL
R^1 ].(1 / 2),(3 / 2).[ is non empty connected V166() V167() V168() interval Element of bool the carrier of K618()
K618() | (R^1 ].(1 / 2),(3 / 2).[) is non empty strict TopSpace-like T_0 T_1 T_2 V211() V271() SubSpace of K618()
the carrier of (K618() | (R^1 ].(1 / 2),(3 / 2).[)) is non empty V166() V167() V168() set
[: the carrier of (Topen_unit_circle c[-10]), the carrier of (K618() | (R^1 ].(1 / 2),(3 / 2).[)):] is Relation-like non empty V156() V157() V158() set
bool [: the carrier of (Topen_unit_circle c[-10]), the carrier of (K618() | (R^1 ].(1 / 2),(3 / 2).[)):] is non empty set
[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is Relation-like non empty set
bool [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is non empty set
[: the carrier of I[01], the carrier of I[01]:] is Relation-like non empty V156() V157() V158() set
bool [: the carrier of I[01], the carrier of I[01]:] is non empty set
bool the carrier of [:I[01],I[01]:] is non empty set
[:COMPLEX,COMPLEX:] is Relation-like non empty V156() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is Relation-like non empty V156() V157() V158() set
bool [:COMPLEX,REAL:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty V156() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:RAT,RAT:] is Relation-like RAT -valued non empty V156() V157() V158() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty V156() V157() V158() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty V156() V157() V158() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty V156() V157() V158() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued V156() V157() V158() V159() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued V156() V157() V158() V159() set
bool [:[:NAT,NAT:],NAT:] is non empty set
[: the carrier of (TOP-REAL 2),REAL:] is Relation-like non empty V156() V157() V158() set
bool [: the carrier of (TOP-REAL 2),REAL:] is non empty set
4 is non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below Element of NAT
sqrt 4 is non empty complex ext-real positive non negative real Element of REAL
the carrier of R^1 is non empty V166() V167() V168() set
R2Homeomorphism is Relation-like the carrier of [:R^1,R^1:] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:R^1,R^1:], the carrier of (TOP-REAL 2):]
[.0,1.] is non empty V166() V167() V168() compact interval Element of bool REAL
0[01] is complex ext-real real Element of the carrier of I[01]
1[01] is complex ext-real real Element of the carrier of I[01]
proj2 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like non empty total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]
proj1 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like non empty total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]
- 1 is complex ext-real non positive real Element of REAL
|[(- 1),0]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
|[1,0]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
R^2-unit_square is functional non empty non trivial closed connected compact bounded being_special_polygon being_simple_closed_curve with_the_max_arc 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 V82() normal T_3 T_4 compact V246() pseudocompact SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | R^2-unit_square) is non empty set
bool the carrier of R^1 is non empty set
Closed-Interval-TSpace ((- 1),1) is non empty strict TopSpace-like T_0 T_1 T_2 V211() SubSpace of R^1
the carrier of (Closed-Interval-TSpace ((- 1),1)) is non empty V166() V167() V168() set
(#) (0,1) is complex ext-real real Element of the carrier of (Closed-Interval-TSpace (0,1))
(0,1) (#) is complex ext-real real Element of the carrier of (Closed-Interval-TSpace (0,1))
{0} is functional non empty V166() V167() V168() V169() V170() V171() left_end bounded_below set
C0 is set
l1 is set
C1 is set
l0 is set
C0 \/ C1 is set
(C0 \/ C1) \/ l0 is set
C0 is set
h1 is set
C1 is set
l0 is set
l1 is set
C0 \/ C1 is set
(C0 \/ C1) \/ l0 is set
((C0 \/ C1) \/ l0) \/ l1 is set
C0 is set
h1 is set
C1 is set
l0 is set
l1 is set
C0 \/ C1 is set
(C0 \/ C1) \/ l0 is set
((C0 \/ C1) \/ l0) \/ l1 is set
C0 is Reflexive symmetric triangle MetrStruct
the carrier of C0 is set
C1 is Element of the carrier of C0
l0 is Element of the carrier of C0
dist (C1,l0) is complex ext-real real Element of REAL
C0 is ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below Element of NAT
TOP-REAL C0 is non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected RLTopStruct
the carrier of (TOP-REAL C0) is functional non empty set
C1 is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
l0 is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
dist (C1,l0) is complex ext-real real Element of REAL
Euclid C0 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of (Euclid C0) is non empty set
l1 is Element of the carrier of (Euclid C0)
h1 is Element of the carrier of (Euclid C0)
dist (l1,h1) is complex ext-real non negative real Element of REAL
C0 is ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below Element of NAT
TOP-REAL C0 is non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected RLTopStruct
the carrier of (TOP-REAL C0) is functional non empty set
C1 is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
l0 is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
C1 + l0 is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
the U7 of (TOP-REAL C0) is Relation-like [: the carrier of (TOP-REAL C0), the carrier of (TOP-REAL C0):] -defined the carrier of (TOP-REAL C0) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (TOP-REAL C0), the carrier of (TOP-REAL C0):], the carrier of (TOP-REAL C0):]
[: the carrier of (TOP-REAL C0), the carrier of (TOP-REAL C0):] is Relation-like non empty set
[:[: the carrier of (TOP-REAL C0), the carrier of (TOP-REAL C0):], the carrier of (TOP-REAL C0):] is Relation-like non empty set
bool [:[: the carrier of (TOP-REAL C0), the carrier of (TOP-REAL C0):], the carrier of (TOP-REAL C0):] is non empty set
K224( the carrier of (TOP-REAL C0), the U7 of (TOP-REAL C0),C1,l0) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
(1 / 2) * (C1 + l0) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
(1 / 2) * C1 is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
(1 / 2) * l0 is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
((1 / 2) * C1) + ((1 / 2) * l0) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K224( the carrier of (TOP-REAL C0), the U7 of (TOP-REAL C0),((1 / 2) * C1),((1 / 2) * l0)) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
0. (TOP-REAL C0) is Relation-like Function-like V49(C0) V50() zero V156() V157() V158() Element of the carrier of (TOP-REAL C0)
the ZeroF of (TOP-REAL C0) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
C1 - (((1 / 2) * C1) + ((1 / 2) * l0)) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
- (((1 / 2) * C1) + ((1 / 2) * l0)) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K270((TOP-REAL C0),C1,(- (((1 / 2) * C1) + ((1 / 2) * l0)))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K224( the carrier of (TOP-REAL C0), the U7 of (TOP-REAL C0),C1,(- (((1 / 2) * C1) + ((1 / 2) * l0)))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
C1 - ((1 / 2) * C1) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
- ((1 / 2) * C1) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K270((TOP-REAL C0),C1,(- ((1 / 2) * C1))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K224( the carrier of (TOP-REAL C0), the U7 of (TOP-REAL C0),C1,(- ((1 / 2) * C1))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
(C1 - ((1 / 2) * C1)) - ((1 / 2) * l0) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
- ((1 / 2) * l0) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K270((TOP-REAL C0),(C1 - ((1 / 2) * C1)),(- ((1 / 2) * l0))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K224( the carrier of (TOP-REAL C0), the U7 of (TOP-REAL C0),(C1 - ((1 / 2) * C1)),(- ((1 / 2) * l0))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
1 * C1 is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
(1 * C1) - ((1 / 2) * C1) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K270((TOP-REAL C0),(1 * C1),(- ((1 / 2) * C1))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K224( the carrier of (TOP-REAL C0), the U7 of (TOP-REAL C0),(1 * C1),(- ((1 / 2) * C1))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
((1 * C1) - ((1 / 2) * C1)) - ((1 / 2) * l0) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K270((TOP-REAL C0),((1 * C1) - ((1 / 2) * C1)),(- ((1 / 2) * l0))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K224( the carrier of (TOP-REAL C0), the U7 of (TOP-REAL C0),((1 * C1) - ((1 / 2) * C1)),(- ((1 / 2) * l0))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
1 - (1 / 2) is complex ext-real real Element of REAL
(1 - (1 / 2)) * C1 is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
((1 - (1 / 2)) * C1) - ((1 / 2) * l0) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K270((TOP-REAL C0),((1 - (1 / 2)) * C1),(- ((1 / 2) * l0))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K224( the carrier of (TOP-REAL C0), the U7 of (TOP-REAL C0),((1 - (1 / 2)) * C1),(- ((1 / 2) * l0))) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
C1 - l0 is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
- l0 is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K270((TOP-REAL C0),C1,(- l0)) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
K224( the carrier of (TOP-REAL C0), the U7 of (TOP-REAL C0),C1,(- l0)) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
(1 / 2) * (C1 - l0) is Relation-like Function-like V49(C0) V50() V156() V157() V158() Element of the carrier of (TOP-REAL C0)
C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
C0 `2 is complex ext-real real Element of REAL
C1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
C1 `2 is complex ext-real real Element of REAL
C0 + C1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):]
[:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is Relation-like non empty set
bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is non empty set
K224( the carrier of (TOP-REAL 2), the U7 of (TOP-REAL 2),C0,C1) is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (C0 + C1) is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (C0 + C1)) `2 is complex ext-real real Element of REAL
(C0 + C1) `2 is complex ext-real real Element of REAL
(1 / 2) * ((C0 + C1) `2) is complex ext-real real Element of REAL
(C0 `2) + (C1 `2) is complex ext-real real Element of REAL
(1 / 2) * ((C0 `2) + (C1 `2)) is complex ext-real real Element of REAL
((C0 `2) + (C1 `2)) / 2 is complex ext-real real Element of REAL
C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
C0 `2 is complex ext-real real Element of REAL
C1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
C1 `2 is complex ext-real real Element of REAL
C0 + C1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):]
[:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is Relation-like non empty set
bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is non empty set
K224( the carrier of (TOP-REAL 2), the U7 of (TOP-REAL 2),C0,C1) is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (C0 + C1) is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (C0 + C1)) `2 is complex ext-real real Element of REAL
(C0 + C1) `2 is complex ext-real real Element of REAL
(1 / 2) * ((C0 + C1) `2) is complex ext-real real Element of REAL
(C0 `2) + (C1 `2) is complex ext-real real Element of REAL
(1 / 2) * ((C0 `2) + (C1 `2)) is complex ext-real real Element of REAL
((C0 `2) + (C1 `2)) / 2 is complex ext-real real Element of REAL
C0 is functional Element of bool the carrier of (TOP-REAL 2)
C1 is functional vertical Element of bool the carrier of (TOP-REAL 2)
C1 /\ C0 is functional Element of bool the carrier of (TOP-REAL 2)
l0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
l1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
l0 `1 is complex ext-real real Element of REAL
l1 `1 is complex ext-real real Element of REAL
C0 is functional Element of bool the carrier of (TOP-REAL 2)
C1 is functional horizontal Element of bool the carrier of (TOP-REAL 2)
C1 /\ C0 is functional Element of bool the carrier of (TOP-REAL 2)
l0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
l1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
l0 `2 is complex ext-real real Element of REAL
l1 `2 is complex ext-real real Element of REAL
C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
C1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
l0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
LSeg (C1,l0) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * C1) + (b1 * l0)) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (C0,l0) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * C0) + (b1 * l0)) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
C1 `1 is complex ext-real real Element of REAL
l0 `1 is complex ext-real real Element of REAL
C0 `1 is complex ext-real real Element of REAL
C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
C1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
l0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
LSeg (C1,l0) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * C1) + (b1 * l0)) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (C0,l0) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * C0) + (b1 * l0)) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
C1 `2 is complex ext-real real Element of REAL
l0 `2 is complex ext-real real Element of REAL
C0 `2 is complex ext-real real Element of REAL
C0 is functional Element of bool the carrier of (TOP-REAL 2)
SW-corner C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
W-bound C0 is complex ext-real real Element of REAL
(TOP-REAL 2) | C0 is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | C0 is Relation-like C0 -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | C0) -defined REAL -valued Function-like total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of ((TOP-REAL 2) | C0),REAL:]
the carrier of ((TOP-REAL 2) | C0) is set
[: the carrier of ((TOP-REAL 2) | C0),REAL:] is Relation-like V156() V157() V158() set
bool [: the carrier of ((TOP-REAL 2) | C0),REAL:] is non empty set
lower_bound (proj1 | C0) is complex ext-real real Element of REAL
(proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0) is V166() V167() V168() Element of bool REAL
K663(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
S-bound C0 is complex ext-real real Element of REAL
proj2 | C0 is Relation-like C0 -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | C0) -defined REAL -valued Function-like total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of ((TOP-REAL 2) | C0),REAL:]
lower_bound (proj2 | C0) is complex ext-real real Element of REAL
(proj2 | C0) .: the carrier of ((TOP-REAL 2) | C0) is V166() V167() V168() Element of bool REAL
K663(((proj2 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
|[(W-bound C0),(S-bound C0)]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
SE-corner C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
E-bound C0 is complex ext-real real Element of REAL
upper_bound (proj1 | C0) is complex ext-real real Element of REAL
K662(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
|[(E-bound C0),(S-bound C0)]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner C0),(SE-corner C0)) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (SW-corner C0)) + (b1 * (SE-corner C0))) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(SW-corner C0) `2 is complex ext-real real Element of REAL
(SE-corner C0) `2 is complex ext-real real Element of REAL
NW-corner C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
N-bound C0 is complex ext-real real Element of REAL
upper_bound (proj2 | C0) is complex ext-real real Element of REAL
K662(((proj2 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
|[(W-bound C0),(N-bound C0)]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
LSeg ((NW-corner C0),(SW-corner C0)) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (NW-corner C0)) + (b1 * (SW-corner C0))) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(NW-corner C0) `1 is complex ext-real real Element of REAL
(SW-corner C0) `1 is complex ext-real real Element of REAL
NE-corner C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
|[(E-bound C0),(N-bound C0)]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
LSeg ((NE-corner C0),(SE-corner C0)) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (NE-corner C0)) + (b1 * (SE-corner C0))) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(NE-corner C0) `1 is complex ext-real real Element of REAL
(SE-corner C0) `1 is complex ext-real real Element of REAL
C0 is functional Element of bool the carrier of (TOP-REAL 2)
SE-corner C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
E-bound C0 is complex ext-real real Element of REAL
(TOP-REAL 2) | C0 is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | C0 is Relation-like C0 -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | C0) -defined REAL -valued Function-like total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of ((TOP-REAL 2) | C0),REAL:]
the carrier of ((TOP-REAL 2) | C0) is set
[: the carrier of ((TOP-REAL 2) | C0),REAL:] is Relation-like V156() V157() V158() set
bool [: the carrier of ((TOP-REAL 2) | C0),REAL:] is non empty set
upper_bound (proj1 | C0) is complex ext-real real Element of REAL
(proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0) is V166() V167() V168() Element of bool REAL
K662(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
S-bound C0 is complex ext-real real Element of REAL
proj2 | C0 is Relation-like C0 -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | C0) -defined REAL -valued Function-like total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of ((TOP-REAL 2) | C0),REAL:]
lower_bound (proj2 | C0) is complex ext-real real Element of REAL
(proj2 | C0) .: the carrier of ((TOP-REAL 2) | C0) is V166() V167() V168() Element of bool REAL
K663(((proj2 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
|[(E-bound C0),(S-bound C0)]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
SW-corner C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
W-bound C0 is complex ext-real real Element of REAL
lower_bound (proj1 | C0) is complex ext-real real Element of REAL
K663(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
|[(W-bound C0),(S-bound C0)]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner C0),(SW-corner C0)) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded horizontal Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (SE-corner C0)) + (b1 * (SW-corner C0))) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
NW-corner C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
N-bound C0 is complex ext-real real Element of REAL
upper_bound (proj2 | C0) is complex ext-real real Element of REAL
K662(((proj2 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
|[(W-bound C0),(N-bound C0)]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner C0),(NW-corner C0)) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded vertical Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (SW-corner C0)) + (b1 * (NW-corner C0))) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
NE-corner C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
|[(E-bound C0),(N-bound C0)]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner C0),(NE-corner C0)) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded vertical Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (SE-corner C0)) + (b1 * (NE-corner C0))) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
C0 is functional Element of bool the carrier of (TOP-REAL 2)
W-bound C0 is complex ext-real real Element of REAL
(TOP-REAL 2) | C0 is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | C0 is Relation-like C0 -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | C0) -defined REAL -valued Function-like total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of ((TOP-REAL 2) | C0),REAL:]
the carrier of ((TOP-REAL 2) | C0) is set
[: the carrier of ((TOP-REAL 2) | C0),REAL:] is Relation-like V156() V157() V158() set
bool [: the carrier of ((TOP-REAL 2) | C0),REAL:] is non empty set
lower_bound (proj1 | C0) is complex ext-real real Element of REAL
(proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0) is V166() V167() V168() Element of bool REAL
K663(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
E-bound C0 is complex ext-real real Element of REAL
upper_bound (proj1 | C0) is complex ext-real real Element of REAL
K662(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
E-min C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
E-most C0 is functional Element of bool the carrier of (TOP-REAL 2)
SE-corner C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
S-bound C0 is complex ext-real real Element of REAL
proj2 | C0 is Relation-like C0 -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | C0) -defined REAL -valued Function-like total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of ((TOP-REAL 2) | C0),REAL:]
lower_bound (proj2 | C0) is complex ext-real real Element of REAL
(proj2 | C0) .: the carrier of ((TOP-REAL 2) | C0) is V166() V167() V168() Element of bool REAL
K663(((proj2 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
|[(E-bound C0),(S-bound C0)]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
NE-corner C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
N-bound C0 is complex ext-real real Element of REAL
upper_bound (proj2 | C0) is complex ext-real real Element of REAL
K662(((proj2 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
|[(E-bound C0),(N-bound C0)]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner C0),(NE-corner C0)) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded vertical Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (SE-corner C0)) + (b1 * (NE-corner C0))) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((SE-corner C0),(NE-corner C0))) /\ C0 is functional Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (E-most C0) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | (E-most C0) is Relation-like E-most C0 -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | (E-most C0)) -defined REAL -valued Function-like total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of ((TOP-REAL 2) | (E-most C0)),REAL:]
the carrier of ((TOP-REAL 2) | (E-most C0)) is set
[: the carrier of ((TOP-REAL 2) | (E-most C0)),REAL:] is Relation-like V156() V157() V158() set
bool [: the carrier of ((TOP-REAL 2) | (E-most C0)),REAL:] is non empty set
lower_bound (proj2 | (E-most C0)) is complex ext-real real Element of REAL
(proj2 | (E-most C0)) .: the carrier of ((TOP-REAL 2) | (E-most C0)) is V166() V167() V168() Element of bool REAL
K663(((proj2 | (E-most C0)) .: the carrier of ((TOP-REAL 2) | (E-most C0)))) is complex ext-real real Element of REAL
|[(E-bound C0),(lower_bound (proj2 | (E-most C0)))]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
(E-min C0) `1 is complex ext-real real Element of REAL
(W-bound C0) + (E-bound C0) is complex ext-real real Element of REAL
((W-bound C0) + (E-bound C0)) / 2 is complex ext-real real Element of REAL
Vertical_Line (((W-bound C0) + (E-bound C0)) / 2) is functional Element of bool the carrier of (TOP-REAL 2)
C0 is complex ext-real real set
Vertical_Line C0 is functional Element of bool the carrier of (TOP-REAL 2)
C1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
C1 `1 is complex ext-real real Element of REAL
l0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
l0 `1 is complex ext-real real Element of REAL
LSeg (C1,l0) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * C1) + (b1 * l0)) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
C0 - (C1 `1) is complex ext-real real Element of REAL
(l0 `1) - (C1 `1) is complex ext-real real Element of REAL
(C0 - (C1 `1)) / ((l0 `1) - (C1 `1)) is complex ext-real real Element of REAL
1 - ((C0 - (C1 `1)) / ((l0 `1) - (C1 `1))) is complex ext-real real Element of REAL
(1 - ((C0 - (C1 `1)) / ((l0 `1) - (C1 `1)))) * C1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
((C0 - (C1 `1)) / ((l0 `1) - (C1 `1))) * l0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
((1 - ((C0 - (C1 `1)) / ((l0 `1) - (C1 `1)))) * C1) + (((C0 - (C1 `1)) / ((l0 `1) - (C1 `1))) * l0) is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):]
[:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is Relation-like non empty set
bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is non empty set
K224( the carrier of (TOP-REAL 2), the U7 of (TOP-REAL 2),((1 - ((C0 - (C1 `1)) / ((l0 `1) - (C1 `1)))) * C1),(((C0 - (C1 `1)) / ((l0 `1) - (C1 `1))) * l0)) is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
(C1 `1) - (C1 `1) is complex ext-real real Element of REAL
(((1 - ((C0 - (C1 `1)) / ((l0 `1) - (C1 `1)))) * C1) + (((C0 - (C1 `1)) / ((l0 `1) - (C1 `1))) * l0)) `1 is complex ext-real real Element of REAL
(1 - ((C0 - (C1 `1)) / ((l0 `1) - (C1 `1)))) * (C1 `1) is complex ext-real real Element of REAL
((C0 - (C1 `1)) / ((l0 `1) - (C1 `1))) * (l0 `1) is complex ext-real real Element of REAL
((1 - ((C0 - (C1 `1)) / ((l0 `1) - (C1 `1)))) * (C1 `1)) + (((C0 - (C1 `1)) / ((l0 `1) - (C1 `1))) * (l0 `1)) is complex ext-real real Element of REAL
((C0 - (C1 `1)) / ((l0 `1) - (C1 `1))) * ((l0 `1) - (C1 `1)) is complex ext-real real Element of REAL
(C1 `1) + (((C0 - (C1 `1)) / ((l0 `1) - (C1 `1))) * ((l0 `1) - (C1 `1))) is complex ext-real real Element of REAL
(C1 `1) + (C0 - (C1 `1)) is complex ext-real real Element of REAL
C0 is complex ext-real real set
Horizontal_Line C0 is functional Element of bool the carrier of (TOP-REAL 2)
C1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
C1 `2 is complex ext-real real Element of REAL
l0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
l0 `2 is complex ext-real real Element of REAL
LSeg (C1,l0) is functional closed closed boundary nowhere_dense connected compact compact bounded bounded Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * C1) + (b1 * l0)) where b1 is complex ext-real real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
C0 - (C1 `2) is complex ext-real real Element of REAL
(l0 `2) - (C1 `2) is complex ext-real real Element of REAL
(C0 - (C1 `2)) / ((l0 `2) - (C1 `2)) is complex ext-real real Element of REAL
1 - ((C0 - (C1 `2)) / ((l0 `2) - (C1 `2))) is complex ext-real real Element of REAL
(1 - ((C0 - (C1 `2)) / ((l0 `2) - (C1 `2)))) * C1 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
((C0 - (C1 `2)) / ((l0 `2) - (C1 `2))) * l0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
((1 - ((C0 - (C1 `2)) / ((l0 `2) - (C1 `2)))) * C1) + (((C0 - (C1 `2)) / ((l0 `2) - (C1 `2))) * l0) is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] -defined the carrier of (TOP-REAL 2) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):]
[:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is Relation-like non empty set
bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is non empty set
K224( the carrier of (TOP-REAL 2), the U7 of (TOP-REAL 2),((1 - ((C0 - (C1 `2)) / ((l0 `2) - (C1 `2)))) * C1),(((C0 - (C1 `2)) / ((l0 `2) - (C1 `2))) * l0)) is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
(C1 `2) - (C1 `2) is complex ext-real real Element of REAL
(((1 - ((C0 - (C1 `2)) / ((l0 `2) - (C1 `2)))) * C1) + (((C0 - (C1 `2)) / ((l0 `2) - (C1 `2))) * l0)) `2 is complex ext-real real Element of REAL
(1 - ((C0 - (C1 `2)) / ((l0 `2) - (C1 `2)))) * (C1 `2) is complex ext-real real Element of REAL
((C0 - (C1 `2)) / ((l0 `2) - (C1 `2))) * (l0 `2) is complex ext-real real Element of REAL
((1 - ((C0 - (C1 `2)) / ((l0 `2) - (C1 `2)))) * (C1 `2)) + (((C0 - (C1 `2)) / ((l0 `2) - (C1 `2))) * (l0 `2)) is complex ext-real real Element of REAL
((C0 - (C1 `2)) / ((l0 `2) - (C1 `2))) * ((l0 `2) - (C1 `2)) is complex ext-real real Element of REAL
(C1 `2) + (((C0 - (C1 `2)) / ((l0 `2) - (C1 `2))) * ((l0 `2) - (C1 `2))) is complex ext-real real Element of REAL
(C1 `2) + (C0 - (C1 `2)) is complex ext-real real Element of REAL
C0 is ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below Element of NAT
TOP-REAL C0 is non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected RLTopStruct
the carrier of (TOP-REAL C0) is functional non empty set
bool the carrier of (TOP-REAL C0) is non empty set
C1 is functional Element of bool the carrier of (TOP-REAL C0)
C1 is functional Element of bool the carrier of (TOP-REAL C0)
C0 is non empty ordinal natural complex ext-real positive non negative real set
TOP-REAL C0 is non empty TopSpace-like T_0 T_1 T_2 V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C0) is functional non empty set
bool the carrier of (TOP-REAL C0) is non empty set
[#] (TOP-REAL C0) is functional non empty non proper non proper open open closed closed dense dense non boundary non boundary connected convex Element of bool the carrier of (TOP-REAL C0)
C1 is ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below Element of NAT
TOP-REAL C1 is non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected RLTopStruct
[#] (TOP-REAL C1) is functional non empty non proper non proper open open closed closed dense dense non boundary non boundary connected a_component convex Element of bool the carrier of (TOP-REAL C1)
the carrier of (TOP-REAL C1) is functional non empty set
bool the carrier of (TOP-REAL C1) is non empty set
C0 is functional closed compact bounded Element of bool the carrier of (TOP-REAL 2)
UMP C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
E-bound C0 is complex ext-real real Element of REAL
(TOP-REAL 2) | C0 is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | C0 is Relation-like C0 -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | C0) -defined REAL -valued Function-like total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of ((TOP-REAL 2) | C0),REAL:]
the carrier of ((TOP-REAL 2) | C0) is set
[: the carrier of ((TOP-REAL 2) | C0),REAL:] is Relation-like V156() V157() V158() set
bool [: the carrier of ((TOP-REAL 2) | C0),REAL:] is non empty set
upper_bound (proj1 | C0) is complex ext-real real Element of REAL
(proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0) is V166() V167() V168() Element of bool REAL
K662(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
W-bound C0 is complex ext-real real Element of REAL
lower_bound (proj1 | C0) is complex ext-real real Element of REAL
K663(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
(E-bound C0) + (W-bound C0) is complex ext-real real Element of REAL
((E-bound C0) + (W-bound C0)) / 2 is complex ext-real real Element of REAL
Vertical_Line (((E-bound C0) + (W-bound C0)) / 2) is functional Element of bool the carrier of (TOP-REAL 2)
C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2)) is functional Element of bool the carrier of (TOP-REAL 2)
proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2))) is V166() V167() V168() Element of bool REAL
K662((proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2))))) is complex ext-real real Element of REAL
|[(((E-bound C0) + (W-bound C0)) / 2),K662((proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2)))))]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
north_halfline (UMP C0) is functional non empty connected convex Element of bool the carrier of (TOP-REAL 2)
{(UMP C0)} is functional non empty closed compact bounded Element of bool the carrier of (TOP-REAL 2)
(north_halfline (UMP C0)) \ {(UMP C0)} is functional Element of bool the carrier of (TOP-REAL 2)
(W-bound C0) + (E-bound C0) is complex ext-real real Element of REAL
((W-bound C0) + (E-bound C0)) / 2 is complex ext-real real Element of REAL
h1 is set
rp is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
rp `1 is complex ext-real real Element of REAL
(UMP C0) `1 is complex ext-real real Element of REAL
(UMP C0) `2 is complex ext-real real Element of REAL
rp `2 is complex ext-real real Element of REAL
Vertical_Line (((W-bound C0) + (E-bound C0)) / 2) is functional Element of bool the carrier of (TOP-REAL 2)
C0 /\ (Vertical_Line (((W-bound C0) + (E-bound C0)) / 2)) is functional Element of bool the carrier of (TOP-REAL 2)
C0 is functional closed compact bounded Element of bool the carrier of (TOP-REAL 2)
LMP C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
E-bound C0 is complex ext-real real Element of REAL
(TOP-REAL 2) | C0 is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | C0 is Relation-like C0 -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | C0) -defined REAL -valued Function-like total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of ((TOP-REAL 2) | C0),REAL:]
the carrier of ((TOP-REAL 2) | C0) is set
[: the carrier of ((TOP-REAL 2) | C0),REAL:] is Relation-like V156() V157() V158() set
bool [: the carrier of ((TOP-REAL 2) | C0),REAL:] is non empty set
upper_bound (proj1 | C0) is complex ext-real real Element of REAL
(proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0) is V166() V167() V168() Element of bool REAL
K662(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
W-bound C0 is complex ext-real real Element of REAL
lower_bound (proj1 | C0) is complex ext-real real Element of REAL
K663(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
(E-bound C0) + (W-bound C0) is complex ext-real real Element of REAL
((E-bound C0) + (W-bound C0)) / 2 is complex ext-real real Element of REAL
Vertical_Line (((E-bound C0) + (W-bound C0)) / 2) is functional Element of bool the carrier of (TOP-REAL 2)
C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2)) is functional Element of bool the carrier of (TOP-REAL 2)
proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2))) is V166() V167() V168() Element of bool REAL
K663((proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2))))) is complex ext-real real Element of REAL
|[(((E-bound C0) + (W-bound C0)) / 2),K663((proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2)))))]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
south_halfline (LMP C0) is functional non empty connected convex Element of bool the carrier of (TOP-REAL 2)
{(LMP C0)} is functional non empty closed compact bounded Element of bool the carrier of (TOP-REAL 2)
(south_halfline (LMP C0)) \ {(LMP C0)} is functional Element of bool the carrier of (TOP-REAL 2)
(W-bound C0) + (E-bound C0) is complex ext-real real Element of REAL
((W-bound C0) + (E-bound C0)) / 2 is complex ext-real real Element of REAL
h1 is set
rp is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
rp `1 is complex ext-real real Element of REAL
(LMP C0) `1 is complex ext-real real Element of REAL
rp `2 is complex ext-real real Element of REAL
(LMP C0) `2 is complex ext-real real Element of REAL
Vertical_Line (((W-bound C0) + (E-bound C0)) / 2) is functional Element of bool the carrier of (TOP-REAL 2)
C0 /\ (Vertical_Line (((W-bound C0) + (E-bound C0)) / 2)) is functional Element of bool the carrier of (TOP-REAL 2)
C0 is functional closed compact bounded Element of bool the carrier of (TOP-REAL 2)
UMP C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
E-bound C0 is complex ext-real real Element of REAL
(TOP-REAL 2) | C0 is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | C0 is Relation-like C0 -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | C0) -defined REAL -valued Function-like total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of ((TOP-REAL 2) | C0),REAL:]
the carrier of ((TOP-REAL 2) | C0) is set
[: the carrier of ((TOP-REAL 2) | C0),REAL:] is Relation-like V156() V157() V158() set
bool [: the carrier of ((TOP-REAL 2) | C0),REAL:] is non empty set
upper_bound (proj1 | C0) is complex ext-real real Element of REAL
(proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0) is V166() V167() V168() Element of bool REAL
K662(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
W-bound C0 is complex ext-real real Element of REAL
lower_bound (proj1 | C0) is complex ext-real real Element of REAL
K663(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
(E-bound C0) + (W-bound C0) is complex ext-real real Element of REAL
((E-bound C0) + (W-bound C0)) / 2 is complex ext-real real Element of REAL
Vertical_Line (((E-bound C0) + (W-bound C0)) / 2) is functional Element of bool the carrier of (TOP-REAL 2)
C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2)) is functional Element of bool the carrier of (TOP-REAL 2)
proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2))) is V166() V167() V168() Element of bool REAL
K662((proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2))))) is complex ext-real real Element of REAL
|[(((E-bound C0) + (W-bound C0)) / 2),K662((proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2)))))]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
north_halfline (UMP C0) is functional non empty connected convex Element of bool the carrier of (TOP-REAL 2)
{(UMP C0)} is functional non empty closed compact bounded Element of bool the carrier of (TOP-REAL 2)
(north_halfline (UMP C0)) \ {(UMP C0)} is functional Element of bool the carrier of (TOP-REAL 2)
UBD C0 is functional non empty open connected being_Region Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_outside_component_of C0 } is set
union { b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_outside_component_of C0 } is set
l0 is functional non empty non bounded Element of bool the carrier of (TOP-REAL 2)
C0 is functional closed compact bounded Element of bool the carrier of (TOP-REAL 2)
LMP C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
E-bound C0 is complex ext-real real Element of REAL
(TOP-REAL 2) | C0 is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | C0 is Relation-like C0 -defined the carrier of (TOP-REAL 2) -defined the carrier of ((TOP-REAL 2) | C0) -defined REAL -valued Function-like total quasi_total V156() V157() V158() continuous Element of bool [: the carrier of ((TOP-REAL 2) | C0),REAL:]
the carrier of ((TOP-REAL 2) | C0) is set
[: the carrier of ((TOP-REAL 2) | C0),REAL:] is Relation-like V156() V157() V158() set
bool [: the carrier of ((TOP-REAL 2) | C0),REAL:] is non empty set
upper_bound (proj1 | C0) is complex ext-real real Element of REAL
(proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0) is V166() V167() V168() Element of bool REAL
K662(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
W-bound C0 is complex ext-real real Element of REAL
lower_bound (proj1 | C0) is complex ext-real real Element of REAL
K663(((proj1 | C0) .: the carrier of ((TOP-REAL 2) | C0))) is complex ext-real real Element of REAL
(E-bound C0) + (W-bound C0) is complex ext-real real Element of REAL
((E-bound C0) + (W-bound C0)) / 2 is complex ext-real real Element of REAL
Vertical_Line (((E-bound C0) + (W-bound C0)) / 2) is functional Element of bool the carrier of (TOP-REAL 2)
C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2)) is functional Element of bool the carrier of (TOP-REAL 2)
proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2))) is V166() V167() V168() Element of bool REAL
K663((proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2))))) is complex ext-real real Element of REAL
|[(((E-bound C0) + (W-bound C0)) / 2),K663((proj2 .: (C0 /\ (Vertical_Line (((E-bound C0) + (W-bound C0)) / 2)))))]| is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
south_halfline (LMP C0) is functional non empty connected convex Element of bool the carrier of (TOP-REAL 2)
{(LMP C0)} is functional non empty closed compact bounded Element of bool the carrier of (TOP-REAL 2)
(south_halfline (LMP C0)) \ {(LMP C0)} is functional Element of bool the carrier of (TOP-REAL 2)
UBD C0 is functional non empty open connected being_Region Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_outside_component_of C0 } is set
union { b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_outside_component_of C0 } is set
l0 is functional non empty non bounded Element of bool the carrier of (TOP-REAL 2)
C0 is functional Element of bool the carrier of (TOP-REAL 2)
C1 is functional Element of bool the carrier of (TOP-REAL 2)
UBD C1 is functional Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_outside_component_of C1 } is set
union { b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_outside_component_of C1 } is set
BDD C1 is functional Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_inside_component_of C1 } is set
union { b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_inside_component_of C1 } is set
C0 is functional Element of bool the carrier of (TOP-REAL 2)
C1 is functional Element of bool the carrier of (TOP-REAL 2)
BDD C1 is functional Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_inside_component_of C1 } is set
union { b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_inside_component_of C1 } is set
UBD C1 is functional Element of bool the carrier of (TOP-REAL 2)
{ b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_outside_component_of C1 } is set
union { b1 where b1 is functional Element of bool the carrier of (TOP-REAL 2) : b1 is_outside_component_of C1 } is set
C0 is Relation-like Function-like V49(2) V50() V156() V157() V158() Element of the carrier of (TOP-REAL 2)
{C0} is functional non empty closed compact bounded Element of bool the carrier of (TOP-REAL 2)
C1 is functional non empty closed connected compact bounded being_simple_closed_curve with_the_max_arc Element of bool the carrier of (TOP-REAL 2)
C1 ` is functional open Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ C1 is set
(TOP-REAL 2) | (C1 `) is strict TopSpace-like T_0 T_1 T_2 V118( TOP-REAL 2) SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (C1 `)) is set
bool the carrier of ((TOP-REAL 2) | (C1 `)) is non empty set
l0 is Element of bool the carrier of ((TOP-REAL 2) | (C1 `))
(#) ((- 1),1) is complex ext-real real Element of the carrier of (Closed-Interval-TSpace ((- 1),1))
((- 1),1) (#) is complex ext-real real Element of the carrier of (Closed-Interval-TSpace ((- 1),1))
L[01] (((#) ((- 1),1)),(((- 1),1) (#))) is Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace ((- 1),1)) -valued Function-like non empty total quasi_total V156() V157() V158() Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace ((- 1),1)):]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace ((- 1),1)):] is Relation-like non empty V156() V157() V158() set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace ((- 1),1)):] is non empty set
[:(TOP-REAL 2),(TOP-REAL 2):] is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] is non empty set
rp is non empty TopSpace-like TopStruct
the carrier of rp is non empty set
rl is complex ext-real real Element of REAL
the carrier of rp --> rl is Relation-like the carrier of rp -defined REAL -valued Function-like non empty total quasi_total V156() V157() V158() Element of bool [: the carrier of rp,REAL:]
[: the carrier of rp,REAL:] is Relation-like non empty V156() V157() V158() set
bool [: the carrier of rp,REAL:] is non empty set
dom ( the carrier of rp --> rl) is non empty Element of bool the carrier of rp
bool the carrier of rp is non empty set
rng ( the carrier of rp --> rl) is non empty V166() V167() V168() Element of bool REAL
{rl} is non empty V166() V167() V168() Element of bool REAL
a is V166() V167() V168() Element of bool REAL
( the carrier of rp --> rl) " a is Element of bool the carrier of rp
(rng ( the carrier of rp --> rl)) /\ a is V166() V167() V168() Element of bool REAL
( the carrier of rp --> rl) " ((rng ( the carrier of rp --> rl)) /\ a) is Element of bool the carrier of rp
( the carrier of rp --> rl) " (rng ( the carrier of rp --> rl)) is Element of bool the carrier of rp
[#] rp is non empty non proper open closed dense non boundary Element of bool the carrier of rp
(rng ( the carrier of rp --> rl)) /\ a is V166() V167() V168() Element of bool REAL
( the carrier of rp --> rl) " ((rng ( the carrier of rp --> rl)) /\ a) is Element of bool the carrier of rp
( the carrier of rp --> rl) " {} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper open closed boundary nowhere_dense connected compact V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval Element of bool the carrier of rp
{} rp is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper open closed boundary nowhere_dense connected compact V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval Element of bool the carrier of rp
rp is ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below Element of NAT
TOP-REAL rp is non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected RLTopStruct
the carrier of (TOP-REAL rp) is functional non empty set
rl is non empty complex ext-real positive non negative real set
rg is Relation-like Function-like V49(rp) V50() V156() V157() V158() Element of the carrier of (TOP-REAL rp)
Ball (rg,rl) is functional non empty open connected bounded convex Element of bool the carrier of (TOP-REAL rp)
bool the carrier of (TOP-REAL rp) is non empty set
rg - rg is Relation-like Function-like V49(rp) V50() V156() V157() V158() Element of the carrier of (TOP-REAL rp)
- rg is Relation-like Function-like V49(rp) V50() V156() V157() V158() Element of the carrier of (TOP-REAL rp)
K270((TOP-REAL rp),rg,(- rg)) is Relation-like Function-like V49(rp) V50() V156() V157() V158() Element of the carrier of (TOP-REAL rp)
the U7 of (TOP-REAL rp) is Relation-like [: the carrier of (TOP-REAL rp), the carrier of (TOP-REAL rp):] -defined the carrier of (TOP-REAL rp) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (TOP-REAL rp), the carrier of (TOP-REAL rp):], the carrier of (TOP-REAL rp):]
[: the carrier of (TOP-REAL rp), the carrier of (TOP-REAL rp):] is Relation-like non empty set
[:[: the carrier of (TOP-REAL rp), the carrier of (