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
{ |[b1,s]| where b1 is V11() real ext-real Element of REAL : not b1 <= C } is set
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 - b1) * n) + (b1 * S1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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
{ |[b1,s]| where b1 is V11() real ext-real Element of REAL : not C <= b1 } is set
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 - b1) * n) + (b1 * S1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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,b1]| where b1 is V11() real ext-real Element of REAL : not b1 <= s } is set
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 - b1) * n) + (b1 * S1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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,b1]| where b1 is V11() real ext-real Element of REAL : not s <= b1 } is set
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 - b1) * n) + (b1 * S1)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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),b1]| where b1 is V11() real ext-real Element of REAL : not b1 <= C `2 } is set
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),b1]| where b1 is V11() real ext-real Element of REAL : not C `2 <= b1 } is set
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
{ |[b1,(C `2)]| where b1 is V11() real ext-real Element of REAL : not C `1 <= b1 } is set
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
{ |[b1,(C `2)]| where b1 is V11() real ext-real Element of REAL : not b1 <= C `1 } is set
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 - b1) * (SW-corner C)) + (b1 * (NW-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SE-corner C)) + (b1 * (NE-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SW-corner C)) + (b1 * (NW-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SE-corner C)) + (b1 * (NE-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SW-corner C)) + (b1 * (NW-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SE-corner C)) + (b1 * (NE-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SE-corner C)) + (b1 * (NE-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SW-corner C)) + (b1 * (NW-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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_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 - b1) * (SE-corner C)) + (b1 * (NE-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SW-corner C)) + (b1 * (NW-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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))
W-min C is V43(2) V97() V140() Element of 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
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 - b1) * (SW-corner C)) + (b1 * (NW-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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-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
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 - b1) * (SE-corner C)) + (b1 * (NE-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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)
Upper_Arc C is non empty closed compact bounded 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))
s is closed connected compact bounded Element of K6( the carrier of (TOP-REAL 2))
S2 is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
{S2} is non empty Element of K6( 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)
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
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
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
E-bound (Lower_Arc C) is V11() real ext-real Element of REAL
upper_bound (proj1 | (Lower_Arc C)) is V11() real ext-real Element of REAL
upper_bound ((proj1 | (Lower_Arc C)) .: the carrier of ((TOP-REAL 2) | (Lower_Arc C))) is V11() real ext-real Element of REAL
(W-bound (Lower_Arc C)) + (E-bound (Lower_Arc C)) is V11() real ext-real Element of REAL
((W-bound (Lower_Arc C)) + (E-bound (Lower_Arc C))) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((W-bound (Lower_Arc C)) + (E-bound (Lower_Arc C))) / 2) is 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
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
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
E-bound (Upper_Arc C) is V11() real ext-real Element of REAL
upper_bound (proj1 | (Upper_Arc C)) is V11() real ext-real Element of REAL
upper_bound ((proj1 | (Upper_Arc C)) .: the carrier of ((TOP-REAL 2) | (Upper_Arc C))) is V11() real ext-real Element of REAL
(W-bound (Upper_Arc C)) + (E-bound (Upper_Arc C)) is V11() real ext-real Element of REAL
((W-bound (Upper_Arc C)) + (E-bound (Upper_Arc C))) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((W-bound (Upper_Arc C)) + (E-bound (Upper_Arc C))) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C is 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
C is non empty closed compact bounded non vertical Element of K6( the carrier of (TOP-REAL 2))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of 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 - b1) * (SW-corner C)) + (b1 * (NW-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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) `1 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
C is non empty closed compact bounded non vertical Element of K6( the carrier of (TOP-REAL 2))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| 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)
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 - b1) * (SE-corner C)) + (b1 * (NE-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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
(C) `1 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
C is non empty closed compact bounded non vertical Element of K6( the carrier of (TOP-REAL 2))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of 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 - b1) * (SW-corner C)) + (b1 * (NW-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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) `1 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
C is non empty closed compact bounded non vertical Element of K6( the carrier of (TOP-REAL 2))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| 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)
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 - b1) * (SE-corner C)) + (b1 * (NE-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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
(C) `1 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
C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
C `2 is V11() real ext-real Element of REAL
s is closed compact bounded Element of K6( the carrier of (TOP-REAL 2))
W-bound s is V11() real ext-real Element of REAL
(TOP-REAL 2) | s is strict T_2 SubSpace of TOP-REAL 2
proj1 | s is V22() V25( the carrier of ((TOP-REAL 2) | s)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | s), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | s),REAL))
the carrier of ((TOP-REAL 2) | s) is set
K7( the carrier of ((TOP-REAL 2) | s),REAL) is V138() V139() V140() set
K6(K7( the carrier of ((TOP-REAL 2) | s),REAL)) is set
lower_bound (proj1 | s) is V11() real ext-real Element of REAL
(proj1 | s) .: the carrier of ((TOP-REAL 2) | s) is V148() V149() V150() Element of K6(REAL)
lower_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
E-bound s is V11() real ext-real Element of REAL
upper_bound (proj1 | s) is V11() real ext-real Element of REAL
upper_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
(W-bound s) + (E-bound s) is V11() real ext-real Element of REAL
((W-bound s) + (E-bound s)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((W-bound s) + (E-bound s)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
s /\ (Vertical_Line (((W-bound s) + (E-bound s)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
(s) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(E-bound s) + (W-bound s) is V11() real ext-real Element of REAL
((E-bound s) + (W-bound s)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound s) + (W-bound s)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound s) + (W-bound s)) / 2),(upper_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(s) `2 is V11() real ext-real Element of REAL
proj2 . C is V11() real ext-real Element of REAL
C is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
C `2 is V11() real ext-real Element of REAL
s is closed compact bounded Element of K6( the carrier of (TOP-REAL 2))
W-bound s is V11() real ext-real Element of REAL
(TOP-REAL 2) | s is strict T_2 SubSpace of TOP-REAL 2
proj1 | s is V22() V25( the carrier of ((TOP-REAL 2) | s)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | s), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | s),REAL))
the carrier of ((TOP-REAL 2) | s) is set
K7( the carrier of ((TOP-REAL 2) | s),REAL) is V138() V139() V140() set
K6(K7( the carrier of ((TOP-REAL 2) | s),REAL)) is set
lower_bound (proj1 | s) is V11() real ext-real Element of REAL
(proj1 | s) .: the carrier of ((TOP-REAL 2) | s) is V148() V149() V150() Element of K6(REAL)
lower_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
E-bound s is V11() real ext-real Element of REAL
upper_bound (proj1 | s) is V11() real ext-real Element of REAL
upper_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
(W-bound s) + (E-bound s) is V11() real ext-real Element of REAL
((W-bound s) + (E-bound s)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((W-bound s) + (E-bound s)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
s /\ (Vertical_Line (((W-bound s) + (E-bound s)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
(s) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(E-bound s) + (W-bound s) is V11() real ext-real Element of REAL
((E-bound s) + (W-bound s)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound s) + (W-bound s)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound s) + (W-bound s)) / 2),(lower_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(s) `2 is V11() real ext-real Element of REAL
proj2 . C is V11() real ext-real Element of REAL
C is non empty closed compact bounded () Element of K6( the carrier of (TOP-REAL 2))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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)
upper_bound (proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
proj2 . n is V11() real ext-real Element of REAL
n `1 is V11() real ext-real Element of REAL
(C) `1 is V11() real ext-real Element of REAL
n `2 is V11() real ext-real Element of REAL
(C) `2 is V11() real ext-real Element of REAL
C is non empty closed compact bounded () Element of K6( the carrier of (TOP-REAL 2))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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)
lower_bound (proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
proj2 . n is V11() real ext-real Element of REAL
n `1 is V11() real ext-real Element of REAL
(C) `1 is V11() real ext-real Element of REAL
n `2 is V11() real ext-real Element of REAL
(C) `2 is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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
N-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))
upper_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)
upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (C)) + (b1 * |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `1 is V11() real ext-real Element of REAL
(C) `1 is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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
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) + (E-bound C)) / 2),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (C)) + (b1 * |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `1 is V11() real ext-real Element of REAL
(C) `1 is V11() real ext-real Element of REAL
C is non empty closed compact bounded () Element of K6( the carrier of (TOP-REAL 2))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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
N-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))
upper_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)
upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (C)) + (b1 * |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|)) /\ C is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
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))
(C) `1 is V11() real ext-real Element of REAL
S is set
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 is V11() real ext-real Element of REAL
(C) `2 is V11() real ext-real Element of REAL
x is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
x `2 is V11() real ext-real Element of REAL
proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
proj2 . x is V11() real ext-real Element of REAL
S is set
C is non empty closed compact bounded () Element of K6( the carrier of (TOP-REAL 2))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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
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) + (E-bound C)) / 2),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (C)) + (b1 * |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
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))
(C) `1 is V11() real ext-real Element of REAL
S is set
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 is V11() real ext-real Element of REAL
(C) `2 is V11() real ext-real Element of REAL
x is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
x `2 is V11() real ext-real Element of REAL
proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
proj2 . x is V11() real ext-real Element of REAL
S is set
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))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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)
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
proj2 . (Lower_Middle_Point C) 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
(Upper_Middle_Point C) `2 is V11() real ext-real Element of REAL
proj2 . (Upper_Middle_Point C) 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))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
(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))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
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
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
N-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))
upper_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)
upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) 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))
S-bound C is V11() real ext-real Element of REAL
(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2
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))
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 (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
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
E-bound C is V11() real ext-real Element of 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))
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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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))
N-bound C is V11() real ext-real Element of REAL
(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2
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))
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 (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)
upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
E-bound C is V11() real ext-real Element of 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))
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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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
N-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))
upper_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)
upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (C)) + (b1 * |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
S-bound C is V11() real ext-real Element of REAL
lower_bound (proj2 | C) is V11() real ext-real Element of REAL
lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (C)) + (b1 * |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
S2 is set
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 is V11() real ext-real Element of REAL
(C) `2 is V11() real ext-real Element of REAL
n is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
n `2 is V11() real ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 is V11() real ext-real Element of REAL
(C) `2 is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
s 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 | 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 s is V11() real ext-real Element of REAL
(TOP-REAL 2) | s is strict T_2 SubSpace of TOP-REAL 2
proj1 | s is V22() V25( the carrier of ((TOP-REAL 2) | s)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | s), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | s),REAL))
the carrier of ((TOP-REAL 2) | s) is set
K7( the carrier of ((TOP-REAL 2) | s),REAL) is V138() V139() V140() set
K6(K7( the carrier of ((TOP-REAL 2) | s),REAL)) is set
lower_bound (proj1 | s) is V11() real ext-real Element of REAL
(proj1 | s) .: the carrier of ((TOP-REAL 2) | s) is V148() V149() V150() Element of K6(REAL)
lower_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
E-bound s is V11() real ext-real Element of REAL
upper_bound (proj1 | s) is V11() real ext-real Element of REAL
upper_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
(W-bound s) + (E-bound s) 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))
s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
(s) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(E-bound s) + (W-bound s) is V11() real ext-real Element of REAL
((E-bound s) + (W-bound s)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound s) + (W-bound s)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound s) + (W-bound s)) / 2),(upper_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(s) `2 is V11() real ext-real Element of REAL
proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
upper_bound (proj2 .: (s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
s 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 | 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 s is V11() real ext-real Element of REAL
(TOP-REAL 2) | s is strict T_2 SubSpace of TOP-REAL 2
proj1 | s is V22() V25( the carrier of ((TOP-REAL 2) | s)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | s), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | s),REAL))
the carrier of ((TOP-REAL 2) | s) is set
K7( the carrier of ((TOP-REAL 2) | s),REAL) is V138() V139() V140() set
K6(K7( the carrier of ((TOP-REAL 2) | s),REAL)) is set
lower_bound (proj1 | s) is V11() real ext-real Element of REAL
(proj1 | s) .: the carrier of ((TOP-REAL 2) | s) is V148() V149() V150() Element of K6(REAL)
lower_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
E-bound s is V11() real ext-real Element of REAL
upper_bound (proj1 | s) is V11() real ext-real Element of REAL
upper_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
(W-bound s) + (E-bound s) 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))
s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
(s) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(E-bound s) + (W-bound s) is V11() real ext-real Element of REAL
((E-bound s) + (W-bound s)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound s) + (W-bound s)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound s) + (W-bound s)) / 2),(lower_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(s) `2 is V11() real ext-real Element of REAL
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
lower_bound (proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
s is Element of K6( the carrier of (TOP-REAL 2))
(s) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
E-bound s is V11() real ext-real Element of REAL
(TOP-REAL 2) | s is strict T_2 SubSpace of TOP-REAL 2
proj1 | s is V22() V25( the carrier of ((TOP-REAL 2) | s)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | s), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | s),REAL))
the carrier of ((TOP-REAL 2) | s) is set
K7( the carrier of ((TOP-REAL 2) | s),REAL) is V138() V139() V140() set
K6(K7( the carrier of ((TOP-REAL 2) | s),REAL)) is set
upper_bound (proj1 | s) is V11() real ext-real Element of REAL
(proj1 | s) .: the carrier of ((TOP-REAL 2) | s) is V148() V149() V150() Element of K6(REAL)
upper_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
W-bound s is V11() real ext-real Element of REAL
lower_bound (proj1 | s) is V11() real ext-real Element of REAL
lower_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
(E-bound s) + (W-bound s) is V11() real ext-real Element of REAL
((E-bound s) + (W-bound s)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound s) + (W-bound s)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound s) + (W-bound s)) / 2),(upper_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))))]| is V43(2) V97() V140() Element of 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 | 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))
(W-bound s) + (E-bound s) is V11() real ext-real Element of REAL
((W-bound s) + (E-bound s)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((W-bound s) + (E-bound s)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
s /\ (Vertical_Line (((W-bound s) + (E-bound s)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((W-bound s) + (E-bound s)) / 2))) is V148() V149() V150() Element of K6(REAL)
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
(s) `1 is V11() real ext-real Element of REAL
(s) `2 is V11() real ext-real Element of REAL
n is V11() real ext-real set
((s) `2) - n is V11() real ext-real Element of REAL
proj2 . (s) is V11() real ext-real Element of REAL
((s) `2) - 0 is V11() real ext-real Element of REAL
s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: (s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
n is V11() real ext-real set
(C) `1 is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
s is Element of K6( the carrier of (TOP-REAL 2))
(s) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
E-bound s is V11() real ext-real Element of REAL
(TOP-REAL 2) | s is strict T_2 SubSpace of TOP-REAL 2
proj1 | s is V22() V25( the carrier of ((TOP-REAL 2) | s)) V26( REAL ) V27() V33( the carrier of ((TOP-REAL 2) | s), REAL ) V138() V139() V140() Element of K6(K7( the carrier of ((TOP-REAL 2) | s),REAL))
the carrier of ((TOP-REAL 2) | s) is set
K7( the carrier of ((TOP-REAL 2) | s),REAL) is V138() V139() V140() set
K6(K7( the carrier of ((TOP-REAL 2) | s),REAL)) is set
upper_bound (proj1 | s) is V11() real ext-real Element of REAL
(proj1 | s) .: the carrier of ((TOP-REAL 2) | s) is V148() V149() V150() Element of K6(REAL)
upper_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
W-bound s is V11() real ext-real Element of REAL
lower_bound (proj1 | s) is V11() real ext-real Element of REAL
lower_bound ((proj1 | s) .: the carrier of ((TOP-REAL 2) | s)) is V11() real ext-real Element of REAL
(E-bound s) + (W-bound s) is V11() real ext-real Element of REAL
((E-bound s) + (W-bound s)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound s) + (W-bound s)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound s) + (W-bound s)) / 2),(lower_bound (proj2 .: (s /\ (Vertical_Line (((E-bound s) + (W-bound s)) / 2)))))]| is V43(2) V97() V140() Element of 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 | 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))
(W-bound s) + (E-bound s) is V11() real ext-real Element of REAL
((W-bound s) + (E-bound s)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((W-bound s) + (E-bound s)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
s /\ (Vertical_Line (((W-bound s) + (E-bound s)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((W-bound s) + (E-bound s)) / 2))) is V148() V149() V150() Element of K6(REAL)
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
(s) `1 is V11() real ext-real Element of REAL
(s) `2 is V11() real ext-real Element of REAL
n is V11() real ext-real set
((s) `2) + n is V11() real ext-real Element of REAL
proj2 . (s) is V11() real ext-real Element of REAL
((s) `2) + 0 is V11() real ext-real Element of REAL
s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (s /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))) is V11() real ext-real Element of REAL
n is V11() real ext-real set
(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))
Upper_Arc C is non empty closed compact bounded () Element of K6( the carrier of (TOP-REAL 2))
((Upper_Arc C)) is V43(2) V97() V140() Element of 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
W-bound (Upper_Arc C) is V11() real ext-real Element of REAL
lower_bound (proj1 | (Upper_Arc C)) is V11() real ext-real Element of REAL
lower_bound ((proj1 | (Upper_Arc C)) .: the carrier of ((TOP-REAL 2) | (Upper_Arc C))) is V11() real ext-real Element of REAL
(E-bound (Upper_Arc C)) + (W-bound (Upper_Arc C)) is V11() real ext-real Element of REAL
((E-bound (Upper_Arc C)) + (W-bound (Upper_Arc C))) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound (Upper_Arc C)) + (W-bound (Upper_Arc C))) / 2) is Element of K6( the carrier of (TOP-REAL 2))
(Upper_Arc C) /\ (Vertical_Line (((E-bound (Upper_Arc C)) + (W-bound (Upper_Arc C))) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound (Upper_Arc C)) + (W-bound (Upper_Arc C))) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound (Upper_Arc C)) + (W-bound (Upper_Arc C))) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound (Upper_Arc C)) + (W-bound (Upper_Arc C))) / 2),(upper_bound (proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound (Upper_Arc C)) + (W-bound (Upper_Arc C))) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
((Upper_Arc C)) `2 is V11() real ext-real Element of REAL
N-bound C is V11() real ext-real Element of REAL
(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2
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))
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 (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)
upper_bound ((proj2 | 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
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))
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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
(Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
upper_bound (proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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))
S-bound C is V11() real ext-real Element of REAL
(TOP-REAL 2) | C is strict T_2 SubSpace of TOP-REAL 2
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))
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 (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
Lower_Arc C is non empty closed compact bounded () Element of K6( the carrier of (TOP-REAL 2))
((Lower_Arc C)) is V43(2) V97() V140() Element of 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
W-bound (Lower_Arc C) is V11() real ext-real Element of REAL
lower_bound (proj1 | (Lower_Arc C)) is V11() real ext-real Element of REAL
lower_bound ((proj1 | (Lower_Arc C)) .: the carrier of ((TOP-REAL 2) | (Lower_Arc C))) is V11() real ext-real Element of REAL
(E-bound (Lower_Arc C)) + (W-bound (Lower_Arc C)) is V11() real ext-real Element of REAL
((E-bound (Lower_Arc C)) + (W-bound (Lower_Arc C))) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound (Lower_Arc C)) + (W-bound (Lower_Arc C))) / 2) is Element of K6( the carrier of (TOP-REAL 2))
(Lower_Arc C) /\ (Vertical_Line (((E-bound (Lower_Arc C)) + (W-bound (Lower_Arc C))) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound (Lower_Arc C)) + (W-bound (Lower_Arc C))) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound (Lower_Arc C)) + (W-bound (Lower_Arc C))) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound (Lower_Arc C)) + (W-bound (Lower_Arc C))) / 2),(lower_bound (proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound (Lower_Arc C)) + (W-bound (Lower_Arc C))) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
((Lower_Arc C)) `2 is V11() real ext-real Element of REAL
E-bound C is V11() real ext-real Element of 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))
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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
(Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
lower_bound (proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(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))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| 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 V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
Upper_Arc C is non empty closed compact bounded () Element of K6( the carrier of (TOP-REAL 2))
(Upper_Arc C) /\ (Lower_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 - b1) * (SW-corner C)) + (b1 * (NW-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SE-corner C)) + (b1 * (NE-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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))
(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
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) + (b1 * (C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 is V11() real ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (C)) + (b1 * |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(W-min C) `1 is V11() real ext-real Element of REAL
(E-max C) `1 is V11() real ext-real Element of REAL
S is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
S `1 is V11() real ext-real Element of REAL
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
S is set
(Lower_Arc C) /\ (Upper_Arc C) is Element of K6( the carrier of (TOP-REAL 2))
(C) `1 is V11() real ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `1 is V11() real ext-real Element of REAL
(C) `1 is V11() real ext-real Element of REAL
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
S is set
(Lower_Arc C) /\ (Upper_Arc C) is Element of K6( the carrier of (TOP-REAL 2))
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `1 is V11() real ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 is V11() real ext-real Element of REAL
S is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
S `2 is V11() real ext-real Element of REAL
Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C)) is Element of K6( the carrier of (TOP-REAL 2))
x is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) is non empty Element of K6( the carrier of (TOP-REAL 2))
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C)))) \/ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is non empty Element of K6( the carrier of (TOP-REAL 2))
x `1 is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
x is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
(C) `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
(Lower_Arc C) \ {(W-min C),(E-max C)} is Element of K6( the carrier of (TOP-REAL 2))
x is set
x is set
(Lower_Arc C) /\ (Upper_Arc C) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))
x is set
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C is Element of K6( the carrier of (TOP-REAL 2))
x is set
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C)))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
(Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) \/ ((Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) is Element of K6( the carrier of (TOP-REAL 2))
{} \/ ((Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) is set
Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C)) is Element of K6( the carrier of (TOP-REAL 2))
x is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) is non empty Element of K6( the carrier of (TOP-REAL 2))
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C)))) \/ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is non empty Element of K6( the carrier of (TOP-REAL 2))
x `1 is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
x is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
(C) `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
(Lower_Arc C) \ {(W-min C),(E-max C)} is Element of K6( the carrier of (TOP-REAL 2))
x is set
x is set
(Lower_Arc C) /\ (Upper_Arc C) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))
x is set
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C is Element of K6( the carrier of (TOP-REAL 2))
x is set
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C)))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
(Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) \/ ((Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) is Element of K6( the carrier of (TOP-REAL 2))
{} \/ ((Segment ((Lower_Arc C),(E-max C),(W-min C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) is set
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))
(C) is V43(2) V97() V140() Element of 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 | 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
W-bound C is V11() real ext-real Element of REAL
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
(E-bound C) + (W-bound C) is V11() real ext-real Element of REAL
((E-bound C) + (W-bound C)) / 2 is V11() real ext-real Element of REAL
Vertical_Line (((E-bound C) + (W-bound C)) / 2) is Element of K6( the carrier of (TOP-REAL 2))
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is V148() V149() V150() Element of K6(REAL)
lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
Upper_Arc C is non empty closed compact bounded () Element of K6( the carrier of (TOP-REAL 2))
(C) is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) is V11() real ext-real Element of REAL
|[(((E-bound C) + (W-bound C)) / 2),(upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))))]| 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))
(Upper_Arc C) /\ (Lower_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 - b1) * (SW-corner C)) + (b1 * (NW-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SE-corner C)) + (b1 * (NE-corner C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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))
(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
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (C)) + (b1 * |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(C) `1 is V11() real ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) + (b1 * (C))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 is V11() real ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `1 is V11() real ext-real Element of REAL
(W-min C) `1 is V11() real ext-real Element of REAL
(E-max C) `1 is V11() real ext-real Element of REAL
S is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
S `1 is V11() real ext-real Element of REAL
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
S is set
(Lower_Arc C) /\ (Upper_Arc C) is Element of K6( the carrier of (TOP-REAL 2))
(C) `1 is V11() real ext-real Element of REAL
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
S is set
(Lower_Arc C) /\ (Upper_Arc C) is Element of K6( the carrier of (TOP-REAL 2))
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `1 is V11() real ext-real Element of REAL
|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 is V11() real ext-real Element of REAL
S is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
S `2 is V11() real ext-real Element of REAL
Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C)) is Element of K6( the carrier of (TOP-REAL 2))
x is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) is non empty Element of K6( the carrier of (TOP-REAL 2))
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C)))) \/ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is non empty Element of K6( the carrier of (TOP-REAL 2))
x `1 is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
x is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
(C) `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
(Upper_Arc C) \ {(W-min C),(E-max C)} is Element of K6( the carrier of (TOP-REAL 2))
x is set
x is set
(Lower_Arc C) /\ (Upper_Arc C) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))
x is set
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C is Element of K6( the carrier of (TOP-REAL 2))
x is set
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C)))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
(Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) \/ ((Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) is Element of K6( the carrier of (TOP-REAL 2))
{} \/ ((Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) is set
Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C)) is Element of K6( the carrier of (TOP-REAL 2))
x is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) is non empty Element of K6( the carrier of (TOP-REAL 2))
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C)))) \/ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is non empty Element of K6( the carrier of (TOP-REAL 2))
x `1 is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
x is V43(2) V97() V140() Element of the carrier of (TOP-REAL 2)
(C) `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
(C) `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
(Upper_Arc C) \ {(W-min C),(E-max C)} is Element of K6( the carrier of (TOP-REAL 2))
x is set
x is set
(Lower_Arc C) /\ (Upper_Arc C) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))
x is set
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) is Element of K6( the carrier of (TOP-REAL 2))
{(C)} is non empty Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C is Element of K6( the carrier of (TOP-REAL 2))
x is set
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C)))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
(Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is Element of K6( the carrier of (TOP-REAL 2))
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) \/ ((Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) is Element of K6( the carrier of (TOP-REAL 2))
{} \/ ((Segment ((Upper_Arc C),(W-min C),(E-max C),(C),(C))) /\ (LSeg ((C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) is set