:: JORDAN21 semantic presentation

REAL is non empty V36() V148() V149() V150() V154() set

NAT is V148() V149() V150() V151() V152() V153() V154() Element of K6(REAL)

K6(REAL) is set

omega is V148() V149() V150() V151() V152() V153() V154() set

K6(omega) is set

1 is non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() Element of NAT

INT is non empty V36() V148() V149() V150() V151() V152() V154() set

K7(1,1) is V26( RAT ) V26( INT ) V138() V139() V140() V141() set

RAT is non empty V36() V148() V149() V150() V151() V154() set

K6(K7(1,1)) is set

K7(K7(1,1),1) is V26( RAT ) V26( INT ) V138() V139() V140() V141() set

K6(K7(K7(1,1),1)) is set

K7(K7(1,1),REAL) is V138() V139() V140() set

K6(K7(K7(1,1),REAL)) is set

K7(REAL,REAL) is V138() V139() V140() set

K7(K7(REAL,REAL),REAL) is V138() V139() V140() set

K6(K7(K7(REAL,REAL),REAL)) is set

2 is non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() Element of NAT

K7(2,2) is V26( RAT ) V26( INT ) V138() V139() V140() V141() set

K7(K7(2,2),REAL) is V138() V139() V140() set

K6(K7(K7(2,2),REAL)) is set

K6(NAT) is set

COMPLEX is non empty V36() V148() V154() set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL 2) is non empty V30() set

K6( the carrier of (TOP-REAL 2)) is set

K7( the carrier of (TOP-REAL 2),REAL) is V138() V139() V140() set

K6(K7( the carrier of (TOP-REAL 2),REAL)) is set

K7(COMPLEX,COMPLEX) is V138() set

K6(K7(COMPLEX,COMPLEX)) is set

K7(COMPLEX,REAL) is V138() V139() V140() set

K6(K7(COMPLEX,REAL)) is set

K7(K7(COMPLEX,COMPLEX),COMPLEX) is V138() set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set

K7(RAT,RAT) is V26( RAT ) V138() V139() V140() set

K6(K7(RAT,RAT)) is set

K7(K7(RAT,RAT),RAT) is V26( RAT ) V138() V139() V140() set

K6(K7(K7(RAT,RAT),RAT)) is set

K7(INT,INT) is V26( RAT ) V26( INT ) V138() V139() V140() set

K6(K7(INT,INT)) is set

K7(K7(INT,INT),INT) is V26( RAT ) V26( INT ) V138() V139() V140() set

K6(K7(K7(INT,INT),INT)) is set

K7(NAT,NAT) is V26( RAT ) V26( INT ) V138() V139() V140() V141() set

K7(K7(NAT,NAT),NAT) is V26( RAT ) V26( INT ) V138() V139() V140() V141() set

K6(K7(K7(NAT,NAT),NAT)) is set

K595() is TopStruct

the carrier of K595() is set

K170() is V79() L7()

K600() is TopSpace-like T_2 TopStruct

{} is empty V148() V149() V150() V151() V152() V153() V154() set

the empty V148() V149() V150() V151() V152() V153() V154() set is empty V148() V149() V150() V151() V152() V153() V154() set

proj2 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

0 is empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() V154() Element of NAT

dom proj2 is Element of K6( the carrier of (TOP-REAL 2))

C is V11() real ext-real set

s is Element of K6( the carrier of (TOP-REAL 2))

proj2 .: s is V148() V149() V150() Element of K6(REAL)

S2 is set

proj2 . S2 is V11() real ext-real Element of REAL

C is set

s is set

S2 is set

s \/ S2 is set

n is set

(s \/ S2) \/ n is set

C is set

n is set

s is set

S2 is set

C \/ s is set

(C \/ s) \/ S2 is set

C is natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() Element of NAT

TOP-REAL C is non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous RLTopStruct

the carrier of (TOP-REAL C) is non empty V30() set

s is V43(C) V97() V140() Element of the carrier of (TOP-REAL C)

{s} is non empty Element of K6( the carrier of (TOP-REAL C))

K6( the carrier of (TOP-REAL C)) is set

Euclid C is non empty V79() V84() V85() V86() V87() L7()

the carrier of (Euclid C) is non empty set

S2 is Element of the carrier of (Euclid C)

{S2} is non empty Element of K6( the carrier of (Euclid C))

K6( the carrier of (Euclid C)) is set

s is V11() real ext-real set

C is V11() real ext-real set

{ |[b

S2 is Element of K6( the carrier of (TOP-REAL 2))

n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg (n,S1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

S is V11() real ext-real Element of REAL

|[S,s]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

x is V11() real ext-real Element of REAL

|[x,s]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 `1 is V11() real ext-real Element of REAL

x is set

l is V11() real ext-real Element of REAL

1 - l is V11() real ext-real Element of REAL

(1 - l) * n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

l * S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

((1 - l) * n) + (l * S1) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

((1 - l) * n) `1 is V11() real ext-real Element of REAL

(l * S1) `1 is V11() real ext-real Element of REAL

(((1 - l) * n) `1) + ((l * S1) `1) is V11() real ext-real Element of REAL

((1 - l) * n) `2 is V11() real ext-real Element of REAL

(l * S1) `2 is V11() real ext-real Element of REAL

(((1 - l) * n) `2) + ((l * S1) `2) is V11() real ext-real Element of REAL

|[((((1 - l) * n) `1) + ((l * S1) `1)),((((1 - l) * n) `2) + ((l * S1) `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

l * (S1 `1) is V11() real ext-real Element of REAL

S1 `2 is V11() real ext-real Element of REAL

l * (S1 `2) is V11() real ext-real Element of REAL

|[(l * (S1 `1)),(l * (S1 `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

n `1 is V11() real ext-real Element of REAL

(1 - l) * (n `1) is V11() real ext-real Element of REAL

n `2 is V11() real ext-real Element of REAL

(1 - l) * (n `2) is V11() real ext-real Element of REAL

|[((1 - l) * (n `1)),((1 - l) * (n `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(((1 - l) * n) + (l * S1)) `1 is V11() real ext-real Element of REAL

((1 - l) * (n `1)) + (l * (S1 `1)) is V11() real ext-real Element of REAL

(((1 - l) * n) + (l * S1)) `2 is V11() real ext-real Element of REAL

((1 - l) * (n `2)) + (l * (S1 `2)) is V11() real ext-real Element of REAL

(1 - l) * s is V11() real ext-real Element of REAL

l * s is V11() real ext-real Element of REAL

((1 - l) * s) + (l * s) is V11() real ext-real Element of REAL

s - 0 is V11() real ext-real Element of REAL

|[((((1 - l) * n) + (l * S1)) `1),((((1 - l) * n) + (l * S1)) `2)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

s is V11() real ext-real set

C is V11() real ext-real set

{ |[b

S2 is Element of K6( the carrier of (TOP-REAL 2))

n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg (n,S1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

S is V11() real ext-real Element of REAL

|[S,s]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

x is V11() real ext-real Element of REAL

|[x,s]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 `1 is V11() real ext-real Element of REAL

x is set

l is V11() real ext-real Element of REAL

1 - l is V11() real ext-real Element of REAL

(1 - l) * n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

l * S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

((1 - l) * n) + (l * S1) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

((1 - l) * n) `1 is V11() real ext-real Element of REAL

(l * S1) `1 is V11() real ext-real Element of REAL

(((1 - l) * n) `1) + ((l * S1) `1) is V11() real ext-real Element of REAL

((1 - l) * n) `2 is V11() real ext-real Element of REAL

(l * S1) `2 is V11() real ext-real Element of REAL

(((1 - l) * n) `2) + ((l * S1) `2) is V11() real ext-real Element of REAL

|[((((1 - l) * n) `1) + ((l * S1) `1)),((((1 - l) * n) `2) + ((l * S1) `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

l * (S1 `1) is V11() real ext-real Element of REAL

S1 `2 is V11() real ext-real Element of REAL

l * (S1 `2) is V11() real ext-real Element of REAL

|[(l * (S1 `1)),(l * (S1 `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

n `1 is V11() real ext-real Element of REAL

(1 - l) * (n `1) is V11() real ext-real Element of REAL

n `2 is V11() real ext-real Element of REAL

(1 - l) * (n `2) is V11() real ext-real Element of REAL

|[((1 - l) * (n `1)),((1 - l) * (n `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(((1 - l) * n) + (l * S1)) `1 is V11() real ext-real Element of REAL

((1 - l) * (n `1)) + (l * (S1 `1)) is V11() real ext-real Element of REAL

(((1 - l) * n) + (l * S1)) `2 is V11() real ext-real Element of REAL

((1 - l) * (n `2)) + (l * (S1 `2)) is V11() real ext-real Element of REAL

(1 - l) * s is V11() real ext-real Element of REAL

l * s is V11() real ext-real Element of REAL

((1 - l) * s) + (l * s) is V11() real ext-real Element of REAL

s - 0 is V11() real ext-real Element of REAL

|[((((1 - l) * n) + (l * S1)) `1),((((1 - l) * n) + (l * S1)) `2)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

C is V11() real ext-real set

s is V11() real ext-real set

{ |[C,b

S2 is Element of K6( the carrier of (TOP-REAL 2))

n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg (n,S1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

S is V11() real ext-real Element of REAL

|[C,S]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

n `1 is V11() real ext-real Element of REAL

x is set

x is V11() real ext-real Element of REAL

1 - x is V11() real ext-real Element of REAL

(1 - x) * n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

x * S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

((1 - x) * n) + (x * S1) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

((1 - x) * n) `1 is V11() real ext-real Element of REAL

(x * S1) `1 is V11() real ext-real Element of REAL

(((1 - x) * n) `1) + ((x * S1) `1) is V11() real ext-real Element of REAL

((1 - x) * n) `2 is V11() real ext-real Element of REAL

(x * S1) `2 is V11() real ext-real Element of REAL

(((1 - x) * n) `2) + ((x * S1) `2) is V11() real ext-real Element of REAL

|[((((1 - x) * n) `1) + ((x * S1) `1)),((((1 - x) * n) `2) + ((x * S1) `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

w is V11() real ext-real Element of REAL

|[C,w]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 `1 is V11() real ext-real Element of REAL

x * (S1 `1) is V11() real ext-real Element of REAL

S1 `2 is V11() real ext-real Element of REAL

x * (S1 `2) is V11() real ext-real Element of REAL

|[(x * (S1 `1)),(x * (S1 `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(1 - x) * (n `1) is V11() real ext-real Element of REAL

n `2 is V11() real ext-real Element of REAL

(1 - x) * (n `2) is V11() real ext-real Element of REAL

|[((1 - x) * (n `1)),((1 - x) * (n `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(((1 - x) * n) + (x * S1)) `2 is V11() real ext-real Element of REAL

((1 - x) * (n `2)) + (x * (S1 `2)) is V11() real ext-real Element of REAL

(((1 - x) * n) + (x * S1)) `1 is V11() real ext-real Element of REAL

|[((((1 - x) * n) + (x * S1)) `1),((((1 - x) * n) + (x * S1)) `2)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

C - 0 is V11() real ext-real Element of REAL

C is V11() real ext-real set

s is V11() real ext-real set

{ |[C,b

S2 is Element of K6( the carrier of (TOP-REAL 2))

n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg (n,S1) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

S is V11() real ext-real Element of REAL

|[C,S]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

x is V11() real ext-real Element of REAL

|[C,x]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 `2 is V11() real ext-real Element of REAL

x is set

l is V11() real ext-real Element of REAL

1 - l is V11() real ext-real Element of REAL

(1 - l) * n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

l * S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

((1 - l) * n) + (l * S1) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

((1 - l) * n) `1 is V11() real ext-real Element of REAL

(l * S1) `1 is V11() real ext-real Element of REAL

(((1 - l) * n) `1) + ((l * S1) `1) is V11() real ext-real Element of REAL

((1 - l) * n) `2 is V11() real ext-real Element of REAL

(l * S1) `2 is V11() real ext-real Element of REAL

(((1 - l) * n) `2) + ((l * S1) `2) is V11() real ext-real Element of REAL

|[((((1 - l) * n) `1) + ((l * S1) `1)),((((1 - l) * n) `2) + ((l * S1) `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 `1 is V11() real ext-real Element of REAL

l * (S1 `1) is V11() real ext-real Element of REAL

l * (S1 `2) is V11() real ext-real Element of REAL

|[(l * (S1 `1)),(l * (S1 `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

n `1 is V11() real ext-real Element of REAL

(1 - l) * (n `1) is V11() real ext-real Element of REAL

n `2 is V11() real ext-real Element of REAL

(1 - l) * (n `2) is V11() real ext-real Element of REAL

|[((1 - l) * (n `1)),((1 - l) * (n `2))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(((1 - l) * n) + (l * S1)) `1 is V11() real ext-real Element of REAL

((1 - l) * (n `1)) + (l * (S1 `1)) is V11() real ext-real Element of REAL

(1 - l) * C is V11() real ext-real Element of REAL

l * C is V11() real ext-real Element of REAL

((1 - l) * C) + (l * C) is V11() real ext-real Element of REAL

C - 0 is V11() real ext-real Element of REAL

(((1 - l) * n) + (l * S1)) `2 is V11() real ext-real Element of REAL

|[((((1 - l) * n) + (l * S1)) `1),((((1 - l) * n) + (l * S1)) `2)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

((1 - l) * (n `2)) + (l * (S1 `2)) is V11() real ext-real Element of REAL

C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

north_halfline C is non empty Element of K6( the carrier of (TOP-REAL 2))

{C} is non empty Element of K6( the carrier of (TOP-REAL 2))

(north_halfline C) \ {C} is Element of K6( the carrier of (TOP-REAL 2))

C `1 is V11() real ext-real Element of REAL

C `2 is V11() real ext-real Element of REAL

{ |[(C `1),b

S2 is set

n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

n `1 is V11() real ext-real Element of REAL

n `2 is V11() real ext-real Element of REAL

|[(C `1),(n `2)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S2 is set

n is V11() real ext-real Element of REAL

|[(C `1),n]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 `2 is V11() real ext-real Element of REAL

S1 `1 is V11() real ext-real Element of REAL

C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

south_halfline C is non empty Element of K6( the carrier of (TOP-REAL 2))

{C} is non empty Element of K6( the carrier of (TOP-REAL 2))

(south_halfline C) \ {C} is Element of K6( the carrier of (TOP-REAL 2))

C `1 is V11() real ext-real Element of REAL

C `2 is V11() real ext-real Element of REAL

{ |[(C `1),b

S2 is set

n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

n `1 is V11() real ext-real Element of REAL

n `2 is V11() real ext-real Element of REAL

|[(C `1),(n `2)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S2 is set

n is V11() real ext-real Element of REAL

|[(C `1),n]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 `2 is V11() real ext-real Element of REAL

S1 `1 is V11() real ext-real Element of REAL

C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

west_halfline C is non empty Element of K6( the carrier of (TOP-REAL 2))

{C} is non empty Element of K6( the carrier of (TOP-REAL 2))

(west_halfline C) \ {C} is Element of K6( the carrier of (TOP-REAL 2))

C `2 is V11() real ext-real Element of REAL

C `1 is V11() real ext-real Element of REAL

{ |[b

S2 is set

n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

n `2 is V11() real ext-real Element of REAL

n `1 is V11() real ext-real Element of REAL

|[(n `1),(C `2)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S2 is set

n is V11() real ext-real Element of REAL

|[n,(C `2)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 `1 is V11() real ext-real Element of REAL

S1 `2 is V11() real ext-real Element of REAL

C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

east_halfline C is non empty Element of K6( the carrier of (TOP-REAL 2))

{C} is non empty Element of K6( the carrier of (TOP-REAL 2))

(east_halfline C) \ {C} is Element of K6( the carrier of (TOP-REAL 2))

C `2 is V11() real ext-real Element of REAL

C `1 is V11() real ext-real Element of REAL

{ |[b

S2 is set

n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

n `2 is V11() real ext-real Element of REAL

n `1 is V11() real ext-real Element of REAL

|[(n `1),(C `2)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S2 is set

n is V11() real ext-real Element of REAL

|[n,(C `2)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 `1 is V11() real ext-real Element of REAL

S1 `2 is V11() real ext-real Element of REAL

C is Element of K6( the carrier of (TOP-REAL 2))

UBD C is Element of K6( the carrier of (TOP-REAL 2))

C ` is Element of K6( the carrier of (TOP-REAL 2))

the carrier of (TOP-REAL 2) \ C is set

C is Element of K6( the carrier of (TOP-REAL 2))

s is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S2 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S1 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

Segment (C,s,S2,n,S1) is Element of K6( the carrier of (TOP-REAL 2))

L_Segment (C,s,S2,S1) is Element of K6( the carrier of (TOP-REAL 2))

R_Segment (C,s,S2,n) is Element of K6( the carrier of (TOP-REAL 2))

(R_Segment (C,s,S2,n)) /\ (L_Segment (C,s,S2,S1)) is Element of K6( the carrier of (TOP-REAL 2))

C is Element of K6( the carrier of (TOP-REAL 2))

W-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj1 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-bound C is V11() real ext-real Element of REAL

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL

((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of REAL

Vertical_Line (((W-bound C) + (E-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))

C is non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

Upper_Middle_Point C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(Upper_Middle_Point C) `1 is V11() real ext-real Element of REAL

W-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj1 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-bound C is V11() real ext-real Element of REAL

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL

((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of REAL

Vertical_Line (((W-bound C) + (E-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))

the non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve () Element of K6( the carrier of (TOP-REAL 2)) is non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve () Element of K6( the carrier of (TOP-REAL 2))

C is non empty () Element of K6( the carrier of (TOP-REAL 2))

W-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj1 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-bound C is V11() real ext-real Element of REAL

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL

((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of REAL

Vertical_Line (((W-bound C) + (E-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))

C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))

proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)

C is closed compact bounded Element of K6( the carrier of (TOP-REAL 2))

W-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj1 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-bound C is V11() real ext-real Element of REAL

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL

((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of REAL

Vertical_Line (((W-bound C) + (E-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))

C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))

proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)

C is non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve () Element of K6( the carrier of (TOP-REAL 2))

Lower_Middle_Point C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

Lower_Arc C is non empty closed compact bounded Element of K6( the carrier of (TOP-REAL 2))

C is non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve () Element of K6( the carrier of (TOP-REAL 2))

Lower_Middle_Point C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(Lower_Middle_Point C) `2 is V11() real ext-real Element of REAL

Upper_Middle_Point C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(Upper_Middle_Point C) `2 is V11() real ext-real Element of REAL

W-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj1 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-bound C is V11() real ext-real Element of REAL

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL

((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of REAL

(Lower_Middle_Point C) `1 is V11() real ext-real Element of REAL

(Upper_Middle_Point C) `1 is V11() real ext-real Element of REAL

Lower_Arc C is non empty closed compact bounded Element of K6( the carrier of (TOP-REAL 2))

Upper_Arc C is non empty closed compact bounded Element of K6( the carrier of (TOP-REAL 2))

(Lower_Arc C) /\ (Upper_Arc C) is Element of K6( the carrier of (TOP-REAL 2))

W-min C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

W-most C is Element of K6( the carrier of (TOP-REAL 2))

SW-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S-bound C is V11() real ext-real Element of REAL

proj2 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(W-bound C),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

NW-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

N-bound C is V11() real ext-real Element of REAL

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(W-bound C),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg ((SW-corner C),(NW-corner C)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

(LSeg ((SW-corner C),(NW-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (W-most C) is strict T_2 SubSpace of TOP-REAL 2

proj2 | (W-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (W-most C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (W-most C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL))

the carrier of ((TOP-REAL 2) | (W-most C)) is set

K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL)) is set

lower_bound (proj2 | (W-most C)) is V11() real ext-real Element of REAL

(proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C)) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C))) is V11() real ext-real Element of REAL

|[(W-bound C),(lower_bound (proj2 | (W-most C)))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

E-max C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

E-most C is Element of K6( the carrier of (TOP-REAL 2))

SE-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

|[(E-bound C),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

NE-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

|[(E-bound C),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg ((SE-corner C),(NE-corner C)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

(LSeg ((SE-corner C),(NE-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (E-most C) is strict T_2 SubSpace of TOP-REAL 2

proj2 | (E-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (E-most C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (E-most C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL))

the carrier of ((TOP-REAL 2) | (E-most C)) is set

K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL)) is set

upper_bound (proj2 | (E-most C)) is V11() real ext-real Element of REAL

(proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C)) is V148() V149() V150() Element of K6(REAL)

upper_bound ((proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C))) is V11() real ext-real Element of REAL

|[(E-bound C),(upper_bound (proj2 | (E-most C)))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

{(W-min C),(E-max C)} is non empty Element of K6( the carrier of (TOP-REAL 2))

C is non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve () Element of K6( the carrier of (TOP-REAL 2))

Lower_Middle_Point C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

Upper_Middle_Point C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(Lower_Middle_Point C) `2 is V11() real ext-real Element of REAL

(Upper_Middle_Point C) `2 is V11() real ext-real Element of REAL

C is non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve () Element of K6( the carrier of (TOP-REAL 2))

W-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj1 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

Upper_Arc C is non empty closed compact bounded Element of K6( the carrier of (TOP-REAL 2))

W-bound (Upper_Arc C) is V11() real ext-real Element of REAL

(TOP-REAL 2) | (Upper_Arc C) is strict T_2 SubSpace of TOP-REAL 2

proj1 | (Upper_Arc C) is V22() V25( the carrier of ((TOP-REAL 2) | (Upper_Arc C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (Upper_Arc C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (Upper_Arc C)),REAL))

the carrier of ((TOP-REAL 2) | (Upper_Arc C)) is set

K7( the carrier of ((TOP-REAL 2) | (Upper_Arc C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (Upper_Arc C)),REAL)) is set

lower_bound (proj1 | (Upper_Arc C)) is V11() real ext-real Element of REAL

(proj1 | (Upper_Arc C)) .: the carrier of ((TOP-REAL 2) | (Upper_Arc C)) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj1 | (Upper_Arc C)) .: the carrier of ((TOP-REAL 2) | (Upper_Arc C))) is V11() real ext-real Element of REAL

W-min C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

W-most C is Element of K6( the carrier of (TOP-REAL 2))

SW-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S-bound C is V11() real ext-real Element of REAL

proj2 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(W-bound C),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

NW-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

N-bound C is V11() real ext-real Element of REAL

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(W-bound C),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg ((SW-corner C),(NW-corner C)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

(LSeg ((SW-corner C),(NW-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (W-most C) is strict T_2 SubSpace of TOP-REAL 2

proj2 | (W-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (W-most C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (W-most C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL))

the carrier of ((TOP-REAL 2) | (W-most C)) is set

K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL)) is set

lower_bound (proj2 | (W-most C)) is V11() real ext-real Element of REAL

(proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C)) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C))) is V11() real ext-real Element of REAL

|[(W-bound C),(lower_bound (proj2 | (W-most C)))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(W-min C) `1 is V11() real ext-real Element of REAL

west_halfline (W-min C) is non empty Element of K6( the carrier of (TOP-REAL 2))

s is set

S2 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S2 `1 is V11() real ext-real Element of REAL

C is non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve () Element of K6( the carrier of (TOP-REAL 2))

E-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj1 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

Upper_Arc C is non empty closed compact bounded Element of K6( the carrier of (TOP-REAL 2))

E-bound (Upper_Arc C) is V11() real ext-real Element of REAL

(TOP-REAL 2) | (Upper_Arc C) is strict T_2 SubSpace of TOP-REAL 2

proj1 | (Upper_Arc C) is V22() V25( the carrier of ((TOP-REAL 2) | (Upper_Arc C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (Upper_Arc C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (Upper_Arc C)),REAL))

the carrier of ((TOP-REAL 2) | (Upper_Arc C)) is set

K7( the carrier of ((TOP-REAL 2) | (Upper_Arc C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (Upper_Arc C)),REAL)) is set

upper_bound (proj1 | (Upper_Arc C)) is V11() real ext-real Element of REAL

(proj1 | (Upper_Arc C)) .: the carrier of ((TOP-REAL 2) | (Upper_Arc C)) is V148() V149() V150() Element of K6(REAL)

upper_bound ((proj1 | (Upper_Arc C)) .: the carrier of ((TOP-REAL 2) | (Upper_Arc C))) is V11() real ext-real Element of REAL

E-max C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

E-most C is Element of K6( the carrier of (TOP-REAL 2))

SE-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S-bound C is V11() real ext-real Element of REAL

proj2 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

NE-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

N-bound C is V11() real ext-real Element of REAL

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg ((SE-corner C),(NE-corner C)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

(LSeg ((SE-corner C),(NE-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (E-most C) is strict T_2 SubSpace of TOP-REAL 2

proj2 | (E-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (E-most C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (E-most C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL))

the carrier of ((TOP-REAL 2) | (E-most C)) is set

K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL)) is set

upper_bound (proj2 | (E-most C)) is V11() real ext-real Element of REAL

(proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C)) is V148() V149() V150() Element of K6(REAL)

upper_bound ((proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C))) is V11() real ext-real Element of REAL

|[(E-bound C),(upper_bound (proj2 | (E-most C)))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(E-max C) `1 is V11() real ext-real Element of REAL

east_halfline (E-max C) is non empty Element of K6( the carrier of (TOP-REAL 2))

s is set

S2 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S2 `1 is V11() real ext-real Element of REAL

C is non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve () Element of K6( the carrier of (TOP-REAL 2))

W-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj1 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

Lower_Arc C is non empty closed compact bounded Element of K6( the carrier of (TOP-REAL 2))

W-bound (Lower_Arc C) is V11() real ext-real Element of REAL

(TOP-REAL 2) | (Lower_Arc C) is strict T_2 SubSpace of TOP-REAL 2

proj1 | (Lower_Arc C) is V22() V25( the carrier of ((TOP-REAL 2) | (Lower_Arc C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (Lower_Arc C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (Lower_Arc C)),REAL))

the carrier of ((TOP-REAL 2) | (Lower_Arc C)) is set

K7( the carrier of ((TOP-REAL 2) | (Lower_Arc C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (Lower_Arc C)),REAL)) is set

lower_bound (proj1 | (Lower_Arc C)) is V11() real ext-real Element of REAL

(proj1 | (Lower_Arc C)) .: the carrier of ((TOP-REAL 2) | (Lower_Arc C)) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj1 | (Lower_Arc C)) .: the carrier of ((TOP-REAL 2) | (Lower_Arc C))) is V11() real ext-real Element of REAL

W-min C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

W-most C is Element of K6( the carrier of (TOP-REAL 2))

SW-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S-bound C is V11() real ext-real Element of REAL

proj2 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(W-bound C),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

NW-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

N-bound C is V11() real ext-real Element of REAL

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(W-bound C),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg ((SW-corner C),(NW-corner C)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

(LSeg ((SW-corner C),(NW-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (W-most C) is strict T_2 SubSpace of TOP-REAL 2

proj2 | (W-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (W-most C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (W-most C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL))

the carrier of ((TOP-REAL 2) | (W-most C)) is set

K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL)) is set

lower_bound (proj2 | (W-most C)) is V11() real ext-real Element of REAL

(proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C)) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C))) is V11() real ext-real Element of REAL

|[(W-bound C),(lower_bound (proj2 | (W-most C)))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(W-min C) `1 is V11() real ext-real Element of REAL

west_halfline (W-min C) is non empty Element of K6( the carrier of (TOP-REAL 2))

s is set

S2 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S2 `1 is V11() real ext-real Element of REAL

C is non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve () Element of K6( the carrier of (TOP-REAL 2))

E-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj1 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

Lower_Arc C is non empty closed compact bounded Element of K6( the carrier of (TOP-REAL 2))

E-bound (Lower_Arc C) is V11() real ext-real Element of REAL

(TOP-REAL 2) | (Lower_Arc C) is strict T_2 SubSpace of TOP-REAL 2

proj1 | (Lower_Arc C) is V22() V25( the carrier of ((TOP-REAL 2) | (Lower_Arc C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (Lower_Arc C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (Lower_Arc C)),REAL))

the carrier of ((TOP-REAL 2) | (Lower_Arc C)) is set

K7( the carrier of ((TOP-REAL 2) | (Lower_Arc C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (Lower_Arc C)),REAL)) is set

upper_bound (proj1 | (Lower_Arc C)) is V11() real ext-real Element of REAL

(proj1 | (Lower_Arc C)) .: the carrier of ((TOP-REAL 2) | (Lower_Arc C)) is V148() V149() V150() Element of K6(REAL)

upper_bound ((proj1 | (Lower_Arc C)) .: the carrier of ((TOP-REAL 2) | (Lower_Arc C))) is V11() real ext-real Element of REAL

E-max C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

E-most C is Element of K6( the carrier of (TOP-REAL 2))

SE-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S-bound C is V11() real ext-real Element of REAL

proj2 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

NE-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

N-bound C is V11() real ext-real Element of REAL

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg ((SE-corner C),(NE-corner C)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

(LSeg ((SE-corner C),(NE-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (E-most C) is strict T_2 SubSpace of TOP-REAL 2

proj2 | (E-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (E-most C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (E-most C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL))

the carrier of ((TOP-REAL 2) | (E-most C)) is set

K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL)) is set

upper_bound (proj2 | (E-most C)) is V11() real ext-real Element of REAL

(proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C)) is V148() V149() V150() Element of K6(REAL)

upper_bound ((proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C))) is V11() real ext-real Element of REAL

|[(E-bound C),(upper_bound (proj2 | (E-most C)))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(E-max C) `1 is V11() real ext-real Element of REAL

east_halfline (E-max C) is non empty Element of K6( the carrier of (TOP-REAL 2))

s is set

S2 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S2 `1 is V11() real ext-real Element of REAL

C is non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve () Element of K6( the carrier of (TOP-REAL 2))

Upper_Arc C is non empty closed compact bounded Element of K6( the carrier of (TOP-REAL 2))

W-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj1 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-bound C is V11() real ext-real Element of REAL

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL

((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of REAL

Vertical_Line (((W-bound C) + (E-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))

(Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))

proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)

E-max C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

E-most C is Element of K6( the carrier of (TOP-REAL 2))

SE-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

S-bound C is V11() real ext-real Element of REAL

proj2 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

NE-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

N-bound C is V11() real ext-real Element of REAL

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(E-bound C),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg ((SE-corner C),(NE-corner C)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

(LSeg ((SE-corner C),(NE-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (E-most C) is strict T_2 SubSpace of TOP-REAL 2

proj2 | (E-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (E-most C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (E-most C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL))

the carrier of ((TOP-REAL 2) | (E-most C)) is set

K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL)) is set

upper_bound (proj2 | (E-most C)) is V11() real ext-real Element of REAL

(proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C)) is V148() V149() V150() Element of K6(REAL)

upper_bound ((proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C))) is V11() real ext-real Element of REAL

|[(E-bound C),(upper_bound (proj2 | (E-most C)))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(E-max C) `1 is V11() real ext-real Element of REAL

W-min C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

W-most C is Element of K6( the carrier of (TOP-REAL 2))

SW-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

|[(W-bound C),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

NW-corner C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

|[(W-bound C),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

LSeg ((SW-corner C),(NW-corner C)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

(LSeg ((SW-corner C),(NW-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (W-most C) is strict T_2 SubSpace of TOP-REAL 2

proj2 | (W-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (W-most C))) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | (W-most C)), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL))

the carrier of ((TOP-REAL 2) | (W-most C)) is set

K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL)) is set

lower_bound (proj2 | (W-most C)) is V11() real ext-real Element of REAL

(proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C)) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C))) is V11() real ext-real Element of REAL

|[(W-bound C),(lower_bound (proj2 | (W-most C)))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)

(W-min C) `1 is V11() real ext-real Element of REAL

C is non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve () Element of K6( the carrier of (TOP-REAL 2))

Lower_Arc C is non empty closed compact bounded Element of K6( the carrier of (TOP-REAL 2))

W-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2

proj1 is V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) V27() V33( the carrier of (TOP-REAL 2), REAL ) V138() V139() V140() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | C), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

the carrier of ((TOP-REAL 2) | C) is set

K7( the carrier of ((TOP-REAL 2) | C),REAL) is V138() V139() V140() set

K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V148() V149() V150() Element of K6(REAL)

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-bound C is V11() real ext-real Element of REAL

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL

((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of REAL

Vertical_Line (((W-bound C) + (E-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))

(Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))

proj2 .: ((Lower_