let a, b, c, d be Real; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[a,c]|,|[b,c]|) & p2 in LSeg (|[a,c]|,|[b,c]|) holds

( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) )

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( a < b & c < d & p1 in LSeg (|[a,c]|,|[b,c]|) & p2 in LSeg (|[a,c]|,|[b,c]|) implies ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) ) )

set K = rectangle (a,b,c,d);

assume that

A1: a < b and

A2: c < d and

A3: p1 in LSeg (|[a,c]|,|[b,c]|) and

A4: p2 in LSeg (|[a,c]|,|[b,c]|) ; :: thesis: ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) )

A5: rectangle (a,b,c,d) is being_simple_closed_curve by A1, A2, Th50;

A6: p1 `2 = c by A1, A3, Th3;

A7: p1 `1 <= b by A1, A3, Th3;

A8: p2 `2 = c by A1, A4, Th3;

A9: a <= p2 `1 by A1, A4, Th3;

A10: W-min (rectangle (a,b,c,d)) = |[a,c]| by A1, A2, Th46;

A11: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;

A12: Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[b,d]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[a,c]|)) by A1, A2, Th52;

then A13: LSeg (|[b,c]|,|[a,c]|) c= Lower_Arc (rectangle (a,b,c,d)) by XBOOLE_1:7;

then A14: p1 in Lower_Arc (rectangle (a,b,c,d)) by A3;

A15: Lower_Arc (rectangle (a,b,c,d)) c= rectangle (a,b,c,d) by A5, JORDAN6:61;

A16: (Upper_Arc (rectangle (a,b,c,d))) /\ (Lower_Arc (rectangle (a,b,c,d))) = {(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d)))} by A5, JORDAN6:def 9;

( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) )

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( a < b & c < d & p1 in LSeg (|[a,c]|,|[b,c]|) & p2 in LSeg (|[a,c]|,|[b,c]|) implies ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) ) )

set K = rectangle (a,b,c,d);

assume that

A1: a < b and

A2: c < d and

A3: p1 in LSeg (|[a,c]|,|[b,c]|) and

A4: p2 in LSeg (|[a,c]|,|[b,c]|) ; :: thesis: ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) )

A5: rectangle (a,b,c,d) is being_simple_closed_curve by A1, A2, Th50;

A6: p1 `2 = c by A1, A3, Th3;

A7: p1 `1 <= b by A1, A3, Th3;

A8: p2 `2 = c by A1, A4, Th3;

A9: a <= p2 `1 by A1, A4, Th3;

A10: W-min (rectangle (a,b,c,d)) = |[a,c]| by A1, A2, Th46;

A11: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;

A12: Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[b,d]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[a,c]|)) by A1, A2, Th52;

then A13: LSeg (|[b,c]|,|[a,c]|) c= Lower_Arc (rectangle (a,b,c,d)) by XBOOLE_1:7;

then A14: p1 in Lower_Arc (rectangle (a,b,c,d)) by A3;

A15: Lower_Arc (rectangle (a,b,c,d)) c= rectangle (a,b,c,d) by A5, JORDAN6:61;

A16: (Upper_Arc (rectangle (a,b,c,d))) /\ (Lower_Arc (rectangle (a,b,c,d))) = {(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d)))} by A5, JORDAN6:def 9;

A17: now :: thesis: ( p1 in Upper_Arc (rectangle (a,b,c,d)) implies p1 = W-min (rectangle (a,b,c,d)) )

thus
( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) implies ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) )
:: thesis: ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) implies ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) ) )assume
p1 in Upper_Arc (rectangle (a,b,c,d))
; :: thesis: p1 = W-min (rectangle (a,b,c,d))

then p1 in (Upper_Arc (rectangle (a,b,c,d))) /\ (Lower_Arc (rectangle (a,b,c,d))) by A3, A13, XBOOLE_0:def 4;

then ( p1 = W-min (rectangle (a,b,c,d)) or p1 = E-max (rectangle (a,b,c,d)) ) by A16, TARSKI:def 2;

hence p1 = W-min (rectangle (a,b,c,d)) by A2, A6, A11, EUCLID:52; :: thesis: verum

end;then p1 in (Upper_Arc (rectangle (a,b,c,d))) /\ (Lower_Arc (rectangle (a,b,c,d))) by A3, A13, XBOOLE_0:def 4;

then ( p1 = W-min (rectangle (a,b,c,d)) or p1 = E-max (rectangle (a,b,c,d)) ) by A16, TARSKI:def 2;

hence p1 = W-min (rectangle (a,b,c,d)) by A2, A6, A11, EUCLID:52; :: thesis: verum

proof

thus
( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) implies ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) ) )
:: thesis: verum
assume that

A18: LE p1,p2, rectangle (a,b,c,d) and

A19: p1 <> W-min (rectangle (a,b,c,d)) ; :: thesis: ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) )

A20: ( ( p1 in Upper_Arc (rectangle (a,b,c,d)) & p2 in Lower_Arc (rectangle (a,b,c,d)) & not p2 = W-min (rectangle (a,b,c,d)) ) or ( p1 in Upper_Arc (rectangle (a,b,c,d)) & p2 in Upper_Arc (rectangle (a,b,c,d)) & LE p1,p2, Upper_Arc (rectangle (a,b,c,d)), W-min (rectangle (a,b,c,d)), E-max (rectangle (a,b,c,d)) ) or ( p1 in Lower_Arc (rectangle (a,b,c,d)) & p2 in Lower_Arc (rectangle (a,b,c,d)) & not p2 = W-min (rectangle (a,b,c,d)) & LE p1,p2, Lower_Arc (rectangle (a,b,c,d)), E-max (rectangle (a,b,c,d)), W-min (rectangle (a,b,c,d)) ) ) by A18, JORDAN6:def 10;

consider f being Function of I[01],((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) such that

A21: f is being_homeomorphism and

A22: f . 0 = E-max (rectangle (a,b,c,d)) and

A23: f . 1 = W-min (rectangle (a,b,c,d)) and

rng f = Lower_Arc (rectangle (a,b,c,d)) and

for r being Real st r in [.0,(1 / 2).] holds

f . r = ((1 - (2 * r)) * |[b,d]|) + ((2 * r) * |[b,c]|) and

for r being Real st r in [.(1 / 2),1.] holds

f . r = ((1 - ((2 * r) - 1)) * |[b,c]|) + (((2 * r) - 1) * |[a,c]|) and

for p being Point of (TOP-REAL 2) st p in LSeg (|[b,d]|,|[b,c]|) holds

( 0 <= (((p `2) - d) / (c - d)) / 2 & (((p `2) - d) / (c - d)) / 2 <= 1 & f . ((((p `2) - d) / (c - d)) / 2) = p ) and

A24: for p being Point of (TOP-REAL 2) st p in LSeg (|[b,c]|,|[a,c]|) holds

( 0 <= ((((p `1) - b) / (a - b)) / 2) + (1 / 2) & ((((p `1) - b) / (a - b)) / 2) + (1 / 2) <= 1 & f . (((((p `1) - b) / (a - b)) / 2) + (1 / 2)) = p ) by A1, A2, Th54;

reconsider s1 = ((((p1 `1) - b) / (a - b)) / 2) + (1 / 2), s2 = ((((p2 `1) - b) / (a - b)) / 2) + (1 / 2) as Real ;

A25: f . s1 = p1 by A3, A24;

A26: f . s2 = p2 by A4, A24;

b - a > 0 by A1, XREAL_1:50;

then A27: - (b - a) < - 0 by XREAL_1:24;

A28: s1 <= 1 by A3, A24;

A29: 0 <= s2 by A4, A24;

s2 <= 1 by A4, A24;

then s1 <= s2 by A17, A19, A20, A21, A22, A23, A25, A26, A28, A29, JORDAN5C:def 3;

then (((p1 `1) - b) / (a - b)) / 2 <= (((p2 `1) - b) / (a - b)) / 2 by XREAL_1:6;

then ((((p1 `1) - b) / (a - b)) / 2) * 2 <= ((((p2 `1) - b) / (a - b)) / 2) * 2 by XREAL_1:64;

then (((p1 `1) - b) / (a - b)) * (a - b) >= (((p2 `1) - b) / (a - b)) * (a - b) by A27, XREAL_1:65;

then (p1 `1) - b >= (((p2 `1) - b) / (a - b)) * (a - b) by A27, XCMPLX_1:87;

then (p1 `1) - b >= (p2 `1) - b by A27, XCMPLX_1:87;

then ((p1 `1) - b) + b >= ((p2 `1) - b) + b by XREAL_1:7;

hence p1 `1 >= p2 `1 ; :: thesis: p2 <> W-min (rectangle (a,b,c,d))

end;A18: LE p1,p2, rectangle (a,b,c,d) and

A19: p1 <> W-min (rectangle (a,b,c,d)) ; :: thesis: ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) )

A20: ( ( p1 in Upper_Arc (rectangle (a,b,c,d)) & p2 in Lower_Arc (rectangle (a,b,c,d)) & not p2 = W-min (rectangle (a,b,c,d)) ) or ( p1 in Upper_Arc (rectangle (a,b,c,d)) & p2 in Upper_Arc (rectangle (a,b,c,d)) & LE p1,p2, Upper_Arc (rectangle (a,b,c,d)), W-min (rectangle (a,b,c,d)), E-max (rectangle (a,b,c,d)) ) or ( p1 in Lower_Arc (rectangle (a,b,c,d)) & p2 in Lower_Arc (rectangle (a,b,c,d)) & not p2 = W-min (rectangle (a,b,c,d)) & LE p1,p2, Lower_Arc (rectangle (a,b,c,d)), E-max (rectangle (a,b,c,d)), W-min (rectangle (a,b,c,d)) ) ) by A18, JORDAN6:def 10;

consider f being Function of I[01],((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) such that

A21: f is being_homeomorphism and

A22: f . 0 = E-max (rectangle (a,b,c,d)) and

A23: f . 1 = W-min (rectangle (a,b,c,d)) and

rng f = Lower_Arc (rectangle (a,b,c,d)) and

for r being Real st r in [.0,(1 / 2).] holds

f . r = ((1 - (2 * r)) * |[b,d]|) + ((2 * r) * |[b,c]|) and

for r being Real st r in [.(1 / 2),1.] holds

f . r = ((1 - ((2 * r) - 1)) * |[b,c]|) + (((2 * r) - 1) * |[a,c]|) and

for p being Point of (TOP-REAL 2) st p in LSeg (|[b,d]|,|[b,c]|) holds

( 0 <= (((p `2) - d) / (c - d)) / 2 & (((p `2) - d) / (c - d)) / 2 <= 1 & f . ((((p `2) - d) / (c - d)) / 2) = p ) and

A24: for p being Point of (TOP-REAL 2) st p in LSeg (|[b,c]|,|[a,c]|) holds

( 0 <= ((((p `1) - b) / (a - b)) / 2) + (1 / 2) & ((((p `1) - b) / (a - b)) / 2) + (1 / 2) <= 1 & f . (((((p `1) - b) / (a - b)) / 2) + (1 / 2)) = p ) by A1, A2, Th54;

reconsider s1 = ((((p1 `1) - b) / (a - b)) / 2) + (1 / 2), s2 = ((((p2 `1) - b) / (a - b)) / 2) + (1 / 2) as Real ;

A25: f . s1 = p1 by A3, A24;

A26: f . s2 = p2 by A4, A24;

b - a > 0 by A1, XREAL_1:50;

then A27: - (b - a) < - 0 by XREAL_1:24;

A28: s1 <= 1 by A3, A24;

A29: 0 <= s2 by A4, A24;

s2 <= 1 by A4, A24;

then s1 <= s2 by A17, A19, A20, A21, A22, A23, A25, A26, A28, A29, JORDAN5C:def 3;

then (((p1 `1) - b) / (a - b)) / 2 <= (((p2 `1) - b) / (a - b)) / 2 by XREAL_1:6;

then ((((p1 `1) - b) / (a - b)) / 2) * 2 <= ((((p2 `1) - b) / (a - b)) / 2) * 2 by XREAL_1:64;

then (((p1 `1) - b) / (a - b)) * (a - b) >= (((p2 `1) - b) / (a - b)) * (a - b) by A27, XREAL_1:65;

then (p1 `1) - b >= (((p2 `1) - b) / (a - b)) * (a - b) by A27, XCMPLX_1:87;

then (p1 `1) - b >= (p2 `1) - b by A27, XCMPLX_1:87;

then ((p1 `1) - b) + b >= ((p2 `1) - b) + b by XREAL_1:7;

hence p1 `1 >= p2 `1 ; :: thesis: p2 <> W-min (rectangle (a,b,c,d))

now :: thesis: not p2 = W-min (rectangle (a,b,c,d))

hence
p2 <> W-min (rectangle (a,b,c,d))
; :: thesis: verumassume A30:
p2 = W-min (rectangle (a,b,c,d))
; :: thesis: contradiction

then LE p2,p1, rectangle (a,b,c,d) by A5, A14, A15, JORDAN7:3;

hence contradiction by A1, A2, A18, A19, A30, Th50, JORDAN6:57; :: thesis: verum

end;then LE p2,p1, rectangle (a,b,c,d) by A5, A14, A15, JORDAN7:3;

hence contradiction by A1, A2, A18, A19, A30, Th50, JORDAN6:57; :: thesis: verum

proof

assume that

A31: p1 `1 >= p2 `1 and

A32: p2 <> W-min (rectangle (a,b,c,d)) ; :: thesis: ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) )

A33: for g being Function of I[01],((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d))))

for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max (rectangle (a,b,c,d)) & g . 1 = W-min (rectangle (a,b,c,d)) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

hence LE p1,p2, rectangle (a,b,c,d) by A3, A4, A13, A32, JORDAN6:def 10; :: thesis: p1 <> W-min (rectangle (a,b,c,d))

thus p1 <> W-min (rectangle (a,b,c,d)) by A93; :: thesis: verum

end;A31: p1 `1 >= p2 `1 and

A32: p2 <> W-min (rectangle (a,b,c,d)) ; :: thesis: ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) )

A33: for g being Function of I[01],((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d))))

for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max (rectangle (a,b,c,d)) & g . 1 = W-min (rectangle (a,b,c,d)) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

proof

let g be Function of I[01],((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))); :: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max (rectangle (a,b,c,d)) & g . 1 = W-min (rectangle (a,b,c,d)) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds

s1 <= s2

let s1, s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = E-max (rectangle (a,b,c,d)) & g . 1 = W-min (rectangle (a,b,c,d)) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )

assume that

A34: g is being_homeomorphism and

A35: g . 0 = E-max (rectangle (a,b,c,d)) and

g . 1 = W-min (rectangle (a,b,c,d)) and

A36: g . s1 = p1 and

A37: 0 <= s1 and

A38: s1 <= 1 and

A39: g . s2 = p2 and

A40: 0 <= s2 and

A41: s2 <= 1 ; :: thesis: s1 <= s2

A42: dom g = the carrier of I[01] by FUNCT_2:def 1;

A43: g is one-to-one by A34, TOPS_2:def 5;

A44: the carrier of ((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) = Lower_Arc (rectangle (a,b,c,d)) by PRE_TOPC:8;

then reconsider g1 = g as Function of I[01],(TOP-REAL 2) by FUNCT_2:7;

g is continuous by A34, TOPS_2:def 5;

then A45: g1 is continuous by PRE_TOPC:26;

reconsider h1 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;

reconsider h2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;

reconsider hh1 = h1 as Function of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #),R^1 ;

reconsider hh2 = h2 as Function of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #),R^1 ;

A46: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) | ([#] TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)) by TSEP_1:3

.= TopStruct(# the carrier of ((TOP-REAL 2) | ([#] (TOP-REAL 2))), the topology of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) #) by PRE_TOPC:36

.= (TOP-REAL 2) | ([#] (TOP-REAL 2)) ;

then ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies hh1 is continuous ) by JGRAPH_2:29;

then A47: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies h1 is continuous ) by PRE_TOPC:32;

( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by A46, JGRAPH_2:30;

then ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by PRE_TOPC:32;

then consider h being Function of (TOP-REAL 2),R^1 such that

A48: for p being Point of (TOP-REAL 2)

for r1, r2 being Real st h1 . p = r1 & h2 . p = r2 holds

h . p = r1 + r2 and

A49: h is continuous by A47, JGRAPH_2:19;

reconsider k = h * g1 as Function of I[01],R^1 ;

A50: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;

end;s1 <= s2

let s1, s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = E-max (rectangle (a,b,c,d)) & g . 1 = W-min (rectangle (a,b,c,d)) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )

assume that

A34: g is being_homeomorphism and

A35: g . 0 = E-max (rectangle (a,b,c,d)) and

g . 1 = W-min (rectangle (a,b,c,d)) and

A36: g . s1 = p1 and

A37: 0 <= s1 and

A38: s1 <= 1 and

A39: g . s2 = p2 and

A40: 0 <= s2 and

A41: s2 <= 1 ; :: thesis: s1 <= s2

A42: dom g = the carrier of I[01] by FUNCT_2:def 1;

A43: g is one-to-one by A34, TOPS_2:def 5;

A44: the carrier of ((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) = Lower_Arc (rectangle (a,b,c,d)) by PRE_TOPC:8;

then reconsider g1 = g as Function of I[01],(TOP-REAL 2) by FUNCT_2:7;

g is continuous by A34, TOPS_2:def 5;

then A45: g1 is continuous by PRE_TOPC:26;

reconsider h1 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;

reconsider h2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;

reconsider hh1 = h1 as Function of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #),R^1 ;

reconsider hh2 = h2 as Function of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #),R^1 ;

A46: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) | ([#] TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)) by TSEP_1:3

.= TopStruct(# the carrier of ((TOP-REAL 2) | ([#] (TOP-REAL 2))), the topology of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) #) by PRE_TOPC:36

.= (TOP-REAL 2) | ([#] (TOP-REAL 2)) ;

then ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies hh1 is continuous ) by JGRAPH_2:29;

then A47: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies h1 is continuous ) by PRE_TOPC:32;

( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by A46, JGRAPH_2:30;

then ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by PRE_TOPC:32;

then consider h being Function of (TOP-REAL 2),R^1 such that

A48: for p being Point of (TOP-REAL 2)

for r1, r2 being Real st h1 . p = r1 & h2 . p = r2 holds

h . p = r1 + r2 and

A49: h is continuous by A47, JGRAPH_2:19;

reconsider k = h * g1 as Function of I[01],R^1 ;

A50: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;

now :: thesis: not s1 > s2

hence
s1 <= s2
; :: thesis: verumassume A51:
s1 > s2
; :: thesis: contradiction

A52: dom g = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;

0 in [.0,1.] by XXREAL_1:1;

then A53: k . 0 = h . (E-max (rectangle (a,b,c,d))) by A35, A52, FUNCT_1:13

.= (h1 . (E-max (rectangle (a,b,c,d)))) + (h2 . (E-max (rectangle (a,b,c,d)))) by A48

.= ((E-max (rectangle (a,b,c,d))) `1) + (proj2 . (E-max (rectangle (a,b,c,d)))) by PSCOMP_1:def 5

.= ((E-max (rectangle (a,b,c,d))) `1) + ((E-max (rectangle (a,b,c,d))) `2) by PSCOMP_1:def 6

.= ((E-max (rectangle (a,b,c,d))) `1) + d by A50, EUCLID:52

.= b + d by A50, EUCLID:52 ;

s1 in [.0,1.] by A37, A38, XXREAL_1:1;

then A54: k . s1 = h . p1 by A36, A52, FUNCT_1:13

.= (proj1 . p1) + (proj2 . p1) by A48

.= (p1 `1) + (proj2 . p1) by PSCOMP_1:def 5

.= (p1 `1) + c by A6, PSCOMP_1:def 6 ;

A55: s2 in [.0,1.] by A40, A41, XXREAL_1:1;

then A56: k . s2 = h . p2 by A39, A52, FUNCT_1:13

.= (h1 . p2) + (h2 . p2) by A48

.= (p2 `1) + (proj2 . p2) by PSCOMP_1:def 5

.= (p2 `1) + c by A8, PSCOMP_1:def 6 ;

A57: k . 0 >= k . s1 by A2, A7, A53, A54, XREAL_1:7;

A58: k . s1 >= k . s2 by A31, A54, A56, XREAL_1:7;

A59: 0 in [.0,1.] by XXREAL_1:1;

then A60: [.0,s2.] c= [.0,1.] by A55, XXREAL_2:def 12;

reconsider B = [.0,s2.] as Subset of I[01] by A55, A59, BORSUK_1:40, XXREAL_2:def 12;

A61: B is connected by A40, A55, A59, BORSUK_1:40, BORSUK_4:24;

A62: 0 in B by A40, XXREAL_1:1;

A63: s2 in B by A40, XXREAL_1:1;

consider xc being Point of I[01] such that

A64: xc in B and

A65: k . xc = k . s1 by A45, A49, A57, A58, A61, A62, A63, TOPREAL5:5;

reconsider rxc = xc as Real ;

A66: for x1, x2 being set st x1 in dom k & x2 in dom k & k . x1 = k . x2 holds

x1 = x2

then s1 in dom k by A37, A38, XXREAL_1:1;

then rxc = s1 by A60, A64, A65, A66, A92;

hence contradiction by A51, A64, XXREAL_1:1; :: thesis: verum

end;A52: dom g = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;

0 in [.0,1.] by XXREAL_1:1;

then A53: k . 0 = h . (E-max (rectangle (a,b,c,d))) by A35, A52, FUNCT_1:13

.= (h1 . (E-max (rectangle (a,b,c,d)))) + (h2 . (E-max (rectangle (a,b,c,d)))) by A48

.= ((E-max (rectangle (a,b,c,d))) `1) + (proj2 . (E-max (rectangle (a,b,c,d)))) by PSCOMP_1:def 5

.= ((E-max (rectangle (a,b,c,d))) `1) + ((E-max (rectangle (a,b,c,d))) `2) by PSCOMP_1:def 6

.= ((E-max (rectangle (a,b,c,d))) `1) + d by A50, EUCLID:52

.= b + d by A50, EUCLID:52 ;

s1 in [.0,1.] by A37, A38, XXREAL_1:1;

then A54: k . s1 = h . p1 by A36, A52, FUNCT_1:13

.= (proj1 . p1) + (proj2 . p1) by A48

.= (p1 `1) + (proj2 . p1) by PSCOMP_1:def 5

.= (p1 `1) + c by A6, PSCOMP_1:def 6 ;

A55: s2 in [.0,1.] by A40, A41, XXREAL_1:1;

then A56: k . s2 = h . p2 by A39, A52, FUNCT_1:13

.= (h1 . p2) + (h2 . p2) by A48

.= (p2 `1) + (proj2 . p2) by PSCOMP_1:def 5

.= (p2 `1) + c by A8, PSCOMP_1:def 6 ;

A57: k . 0 >= k . s1 by A2, A7, A53, A54, XREAL_1:7;

A58: k . s1 >= k . s2 by A31, A54, A56, XREAL_1:7;

A59: 0 in [.0,1.] by XXREAL_1:1;

then A60: [.0,s2.] c= [.0,1.] by A55, XXREAL_2:def 12;

reconsider B = [.0,s2.] as Subset of I[01] by A55, A59, BORSUK_1:40, XXREAL_2:def 12;

A61: B is connected by A40, A55, A59, BORSUK_1:40, BORSUK_4:24;

A62: 0 in B by A40, XXREAL_1:1;

A63: s2 in B by A40, XXREAL_1:1;

consider xc being Point of I[01] such that

A64: xc in B and

A65: k . xc = k . s1 by A45, A49, A57, A58, A61, A62, A63, TOPREAL5:5;

reconsider rxc = xc as Real ;

A66: for x1, x2 being set st x1 in dom k & x2 in dom k & k . x1 = k . x2 holds

x1 = x2

proof

A92:
dom k = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
let x1, x2 be set ; :: thesis: ( x1 in dom k & x2 in dom k & k . x1 = k . x2 implies x1 = x2 )

assume that

A67: x1 in dom k and

A68: x2 in dom k and

A69: k . x1 = k . x2 ; :: thesis: x1 = x2

reconsider r1 = x1 as Point of I[01] by A67;

reconsider r2 = x2 as Point of I[01] by A68;

A70: k . x1 = h . (g1 . x1) by A67, FUNCT_1:12

.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A48

.= ((g1 . r1) `1) + (proj2 . (g1 . r1)) by PSCOMP_1:def 5

.= ((g1 . r1) `1) + ((g1 . r1) `2) by PSCOMP_1:def 6 ;

A71: k . x2 = h . (g1 . x2) by A68, FUNCT_1:12

.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A48

.= ((g1 . r2) `1) + (proj2 . (g1 . r2)) by PSCOMP_1:def 5

.= ((g1 . r2) `1) + ((g1 . r2) `2) by PSCOMP_1:def 6 ;

A72: g . r1 in Lower_Arc (rectangle (a,b,c,d)) by A44;

A73: g . r2 in Lower_Arc (rectangle (a,b,c,d)) by A44;

reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A72;

reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A73;

end;assume that

A67: x1 in dom k and

A68: x2 in dom k and

A69: k . x1 = k . x2 ; :: thesis: x1 = x2

reconsider r1 = x1 as Point of I[01] by A67;

reconsider r2 = x2 as Point of I[01] by A68;

A70: k . x1 = h . (g1 . x1) by A67, FUNCT_1:12

.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A48

.= ((g1 . r1) `1) + (proj2 . (g1 . r1)) by PSCOMP_1:def 5

.= ((g1 . r1) `1) + ((g1 . r1) `2) by PSCOMP_1:def 6 ;

A71: k . x2 = h . (g1 . x2) by A68, FUNCT_1:12

.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A48

.= ((g1 . r2) `1) + (proj2 . (g1 . r2)) by PSCOMP_1:def 5

.= ((g1 . r2) `1) + ((g1 . r2) `2) by PSCOMP_1:def 6 ;

A72: g . r1 in Lower_Arc (rectangle (a,b,c,d)) by A44;

A73: g . r2 in Lower_Arc (rectangle (a,b,c,d)) by A44;

reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A72;

reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A73;

now :: thesis: ( ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) & x1 = x2 ) or ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) & x1 = x2 ) or ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) & x1 = x2 ) or ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) & x1 = x2 ) )end;

hence
x1 = x2
; :: thesis: verumper cases
( ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) ) or ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) or ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) ) or ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) )
by A12, A44, XBOOLE_0:def 3;

end;

case A74:
( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) )
; :: thesis: x1 = x2

then A75:
gr1 `1 = b
by A2, Th1;

gr2 `1 = b by A2, A74, Th1;

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A69, A70, A71, A75, EUCLID:53;

then g . r1 = g . r2 by EUCLID:53;

hence x1 = x2 by A42, A43, FUNCT_1:def 4; :: thesis: verum

end;gr2 `1 = b by A2, A74, Th1;

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A69, A70, A71, A75, EUCLID:53;

then g . r1 = g . r2 by EUCLID:53;

hence x1 = x2 by A42, A43, FUNCT_1:def 4; :: thesis: verum

case A76:
( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) )
; :: thesis: x1 = x2

then A77:
gr1 `1 = b
by A2, Th1;

A78: c <= gr1 `2 by A2, A76, Th1;

A79: gr2 `2 = c by A1, A76, Th3;

A80: gr2 `1 <= b by A1, A76, Th3;

A81: b + (gr1 `2) = (gr2 `1) + c by A1, A69, A70, A71, A76, A77, Th3;

then g . r1 = g . r2 by EUCLID:53;

hence x1 = x2 by A42, A43, FUNCT_1:def 4; :: thesis: verum

end;A78: c <= gr1 `2 by A2, A76, Th1;

A79: gr2 `2 = c by A1, A76, Th3;

A80: gr2 `1 <= b by A1, A76, Th3;

A81: b + (gr1 `2) = (gr2 `1) + c by A1, A69, A70, A71, A76, A77, Th3;

A82: now :: thesis: not b <> gr2 `1

assume
b <> gr2 `1
; :: thesis: contradiction

then b > gr2 `1 by A80, XXREAL_0:1;

hence contradiction by A78, A81, XREAL_1:8; :: thesis: verum

end;then b > gr2 `1 by A80, XXREAL_0:1;

hence contradiction by A78, A81, XREAL_1:8; :: thesis: verum

now :: thesis: not gr1 `2 <> c

then
|[(gr1 `1),(gr1 `2)]| = g . r2
by A77, A79, A82, EUCLID:53;assume
gr1 `2 <> c
; :: thesis: contradiction

then c < gr1 `2 by A78, XXREAL_0:1;

hence contradiction by A69, A70, A71, A77, A79, A80, XREAL_1:8; :: thesis: verum

end;then c < gr1 `2 by A78, XXREAL_0:1;

hence contradiction by A69, A70, A71, A77, A79, A80, XREAL_1:8; :: thesis: verum

then g . r1 = g . r2 by EUCLID:53;

hence x1 = x2 by A42, A43, FUNCT_1:def 4; :: thesis: verum

case A83:
( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) )
; :: thesis: x1 = x2

then A84:
gr2 `1 = b
by A2, Th1;

A85: c <= gr2 `2 by A2, A83, Th1;

A86: gr1 `2 = c by A1, A83, Th3;

A87: gr1 `1 <= b by A1, A83, Th3;

A88: b + (gr2 `2) = (gr1 `1) + c by A1, A69, A70, A71, A83, A84, Th3;

then g . r1 = g . r2 by EUCLID:53;

hence x1 = x2 by A42, A43, FUNCT_1:def 4; :: thesis: verum

end;A85: c <= gr2 `2 by A2, A83, Th1;

A86: gr1 `2 = c by A1, A83, Th3;

A87: gr1 `1 <= b by A1, A83, Th3;

A88: b + (gr2 `2) = (gr1 `1) + c by A1, A69, A70, A71, A83, A84, Th3;

A89: now :: thesis: not b <> gr1 `1

assume
b <> gr1 `1
; :: thesis: contradiction

then b > gr1 `1 by A87, XXREAL_0:1;

hence contradiction by A85, A88, XREAL_1:8; :: thesis: verum

end;then b > gr1 `1 by A87, XXREAL_0:1;

hence contradiction by A85, A88, XREAL_1:8; :: thesis: verum

now :: thesis: not gr2 `2 <> c

then
|[(gr2 `1),(gr2 `2)]| = g . r1
by A84, A86, A89, EUCLID:53;assume
gr2 `2 <> c
; :: thesis: contradiction

then c < gr2 `2 by A85, XXREAL_0:1;

hence contradiction by A69, A70, A71, A84, A86, A87, XREAL_1:8; :: thesis: verum

end;then c < gr2 `2 by A85, XXREAL_0:1;

hence contradiction by A69, A70, A71, A84, A86, A87, XREAL_1:8; :: thesis: verum

then g . r1 = g . r2 by EUCLID:53;

hence x1 = x2 by A42, A43, FUNCT_1:def 4; :: thesis: verum

case A90:
( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) )
; :: thesis: x1 = x2

then A91:
gr1 `2 = c
by A1, Th3;

gr2 `2 = c by A1, A90, Th3;

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A69, A70, A71, A91, EUCLID:53;

then g . r1 = g . r2 by EUCLID:53;

hence x1 = x2 by A42, A43, FUNCT_1:def 4; :: thesis: verum

end;gr2 `2 = c by A1, A90, Th3;

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A69, A70, A71, A91, EUCLID:53;

then g . r1 = g . r2 by EUCLID:53;

hence x1 = x2 by A42, A43, FUNCT_1:def 4; :: thesis: verum

then s1 in dom k by A37, A38, XXREAL_1:1;

then rxc = s1 by A60, A64, A65, A66, A92;

hence contradiction by A51, A64, XXREAL_1:1; :: thesis: verum

A93: now :: thesis: not p1 = W-min (rectangle (a,b,c,d))

LE p1,p2, Lower_Arc (rectangle (a,b,c,d)), E-max (rectangle (a,b,c,d)), W-min (rectangle (a,b,c,d))
by A3, A4, A13, A33, JORDAN5C:def 3;assume A94:
p1 = W-min (rectangle (a,b,c,d))
; :: thesis: contradiction

then p1 `1 = a by A10, EUCLID:52;

then p1 `1 = p2 `1 by A9, A31, XXREAL_0:1;

then |[(p1 `1),(p1 `2)]| = p2 by A6, A8, EUCLID:53;

hence contradiction by A32, A94, EUCLID:53; :: thesis: verum

end;then p1 `1 = a by A10, EUCLID:52;

then p1 `1 = p2 `1 by A9, A31, XXREAL_0:1;

then |[(p1 `1),(p1 `2)]| = p2 by A6, A8, EUCLID:53;

hence contradiction by A32, A94, EUCLID:53; :: thesis: verum

hence LE p1,p2, rectangle (a,b,c,d) by A3, A4, A13, A32, JORDAN6:def 10; :: thesis: p1 <> W-min (rectangle (a,b,c,d))

thus p1 <> W-min (rectangle (a,b,c,d)) by A93; :: thesis: verum