:: JORDAN semantic presentation

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

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

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

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

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

(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 - b

(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 - b

(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 - b

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

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

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

(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 - b

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

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)

{ b

union { b

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)

{ b

union { b

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)

{ b

union { b

BDD C1 is functional Element of bool the carrier of (TOP-REAL 2)

{ b

union { b

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)

{ b

union { b

UBD C1 is functional Element of bool the carrier of (TOP-REAL 2)

{ b

union { b

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 (