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 (|[b,c]|,|[a,c]|) & p1 <> W-min (rectangle (a,b,c,d)) holds

( LE p1,p2, rectangle (a,b,c,d) iff ( p2 in LSeg (|[b,c]|,|[a,c]|) & 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 (|[b,c]|,|[a,c]|) & p1 <> W-min (rectangle (a,b,c,d)) implies ( LE p1,p2, rectangle (a,b,c,d) iff ( p2 in LSeg (|[b,c]|,|[a,c]|) & 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 (|[b,c]|,|[a,c]|) and

A4: p1 <> W-min (rectangle (a,b,c,d)) ; :: thesis: ( LE p1,p2, rectangle (a,b,c,d) iff ( p2 in LSeg (|[b,c]|,|[a,c]|) & 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;

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

( LE p1,p2, rectangle (a,b,c,d) iff ( p2 in LSeg (|[b,c]|,|[a,c]|) & 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 (|[b,c]|,|[a,c]|) & p1 <> W-min (rectangle (a,b,c,d)) implies ( LE p1,p2, rectangle (a,b,c,d) iff ( p2 in LSeg (|[b,c]|,|[a,c]|) & 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 (|[b,c]|,|[a,c]|) and

A4: p1 <> W-min (rectangle (a,b,c,d)) ; :: thesis: ( LE p1,p2, rectangle (a,b,c,d) iff ( p2 in LSeg (|[b,c]|,|[a,c]|) & 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;

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

proof

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

then A9: p2 in rectangle (a,b,c,d) by A5, JORDAN7:5;

rectangle (a,b,c,d) = ((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ ((LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|))) by SPPOL_2:def 3

.= (((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ (LSeg (|[b,d]|,|[b,c]|))) \/ (LSeg (|[b,c]|,|[a,c]|)) by XBOOLE_1:4 ;

then ( p2 in ((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ (LSeg (|[b,d]|,|[b,c]|)) or p2 in LSeg (|[b,c]|,|[a,c]|) ) by A9, XBOOLE_0:def 3;

then A10: ( p2 in (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) or p2 in LSeg (|[b,d]|,|[b,c]|) or p2 in LSeg (|[b,c]|,|[a,c]|) ) by XBOOLE_0:def 3;

end;then A9: p2 in rectangle (a,b,c,d) by A5, JORDAN7:5;

rectangle (a,b,c,d) = ((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ ((LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|))) by SPPOL_2:def 3

.= (((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ (LSeg (|[b,d]|,|[b,c]|))) \/ (LSeg (|[b,c]|,|[a,c]|)) by XBOOLE_1:4 ;

then ( p2 in ((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ (LSeg (|[b,d]|,|[b,c]|)) or p2 in LSeg (|[b,c]|,|[a,c]|) ) by A9, XBOOLE_0:def 3;

then A10: ( p2 in (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) or p2 in LSeg (|[b,d]|,|[b,c]|) or p2 in LSeg (|[b,c]|,|[a,c]|) ) by XBOOLE_0:def 3;

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

hence
( p2 in LSeg (|[b,c]|,|[a,c]|) & p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) )
; :: thesis: verumper cases
( p2 in LSeg (|[a,c]|,|[a,d]|) or p2 in LSeg (|[a,d]|,|[b,d]|) or p2 in LSeg (|[b,d]|,|[b,c]|) or p2 in LSeg (|[b,c]|,|[a,c]|) )
by A10, XBOOLE_0:def 3;

end;

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

then
LE p2,p1, rectangle (a,b,c,d)
by A1, A2, A3, A4, Th59;

hence ( p2 in LSeg (|[b,c]|,|[a,c]|) & p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) by A1, A2, A3, A4, A8, Th50, JORDAN6:57; :: thesis: verum

end;hence ( p2 in LSeg (|[b,c]|,|[a,c]|) & p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) by A1, A2, A3, A4, A8, Th50, JORDAN6:57; :: thesis: verum

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

then
LE p2,p1, rectangle (a,b,c,d)
by A1, A2, A3, A4, Th60;

hence ( p2 in LSeg (|[b,c]|,|[a,c]|) & p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) by A1, A2, A3, A4, A8, Th50, JORDAN6:57; :: thesis: verum

end;hence ( p2 in LSeg (|[b,c]|,|[a,c]|) & p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) by A1, A2, A3, A4, A8, Th50, JORDAN6:57; :: thesis: verum

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

then
LE p2,p1, rectangle (a,b,c,d)
by A1, A2, A3, A4, Th61;

hence ( p2 in LSeg (|[b,c]|,|[a,c]|) & p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) by A1, A2, A3, A4, A8, Th50, JORDAN6:57; :: thesis: verum

end;hence ( p2 in LSeg (|[b,c]|,|[a,c]|) & p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) by A1, A2, A3, A4, A8, Th50, JORDAN6:57; :: thesis: verum

proof

assume that

A11: p2 in LSeg (|[b,c]|,|[a,c]|) and

A12: p1 `1 >= p2 `1 and

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

end;A11: p2 in LSeg (|[b,c]|,|[a,c]|) and

A12: p1 `1 >= p2 `1 and

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

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

hence
LE p1,p2, rectangle (a,b,c,d)
; :: thesis: verumper cases
( ( p2 in LSeg (|[b,c]|,|[a,c]|) & p1 `1 >= p2 `1 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )
by A11, A12;

end;

case A14:
( p2 in LSeg (|[b,c]|,|[a,c]|) & p1 `1 >= p2 `1 )
; :: thesis: LE p1,p2, rectangle (a,b,c,d)

then A15:
p2 `2 = c
by A1, Th3;

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

then A17: p2 in Lower_Arc (rectangle (a,b,c,d)) by A14, XBOOLE_0:def 3;

A18: p1 in Lower_Arc (rectangle (a,b,c,d)) by A3, A16, XBOOLE_0:def 3;

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 A13, A17, A18, JORDAN6:def 10; :: thesis: verum

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

then A17: p2 in Lower_Arc (rectangle (a,b,c,d)) by A14, XBOOLE_0:def 3;

A18: p1 in Lower_Arc (rectangle (a,b,c,d)) by A3, A16, XBOOLE_0:def 3;

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

then
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 A17, A18, JORDAN5C:def 3;
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

A19: g is being_homeomorphism and

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

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

A21: g . s1 = p1 and

A22: 0 <= s1 and

A23: s1 <= 1 and

A24: g . s2 = p2 and

A25: 0 <= s2 and

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

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

A28: g is one-to-one by A19, TOPS_2:def 5;

A29: 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 A19, TOPS_2:def 5;

then A30: 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 ;

A31: 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 A32: ( ( 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 A31, 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

A33: 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

A34: h is continuous by A32, JGRAPH_2:19;

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

A35: 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

A19: g is being_homeomorphism and

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

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

A21: g . s1 = p1 and

A22: 0 <= s1 and

A23: s1 <= 1 and

A24: g . s2 = p2 and

A25: 0 <= s2 and

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

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

A28: g is one-to-one by A19, TOPS_2:def 5;

A29: 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 A19, TOPS_2:def 5;

then A30: 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 ;

A31: 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 A32: ( ( 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 A31, 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

A33: 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

A34: h is continuous by A32, JGRAPH_2:19;

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

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

now :: thesis: not s1 > s2

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

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

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

then A38: k . 0 = h . (E-max (rectangle (a,b,c,d))) by A20, A37, FUNCT_1:13

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

.= ((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 A35, EUCLID:52

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

s1 in [.0,1.] by A22, A23, XXREAL_1:1;

then A39: k . s1 = h . p1 by A21, A37, FUNCT_1:13

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

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

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

A40: s2 in [.0,1.] by A25, A26, XXREAL_1:1;

then A41: k . s2 = h . p2 by A24, A37, FUNCT_1:13

.= (proj1 . p2) + (proj2 . p2) by A33

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

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

A42: k . 0 >= k . s1 by A2, A7, A38, A39, XREAL_1:7;

A43: k . s1 >= k . s2 by A14, A39, A41, XREAL_1:7;

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

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

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

A46: B is connected by A25, A40, A44, BORSUK_1:40, BORSUK_4:24;

A47: 0 in B by A25, XXREAL_1:1;

A48: s2 in B by A25, XXREAL_1:1;

consider xc being Point of I[01] such that

A49: xc in B and

A50: k . xc = k . s1 by A30, A34, A42, A43, A46, A47, A48, TOPREAL5:5;

reconsider rxc = xc as Real ;

A51: 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 A22, A23, XXREAL_1:1;

then rxc = s1 by A45, A49, A50, A51, A77;

hence contradiction by A36, A49, XXREAL_1:1; :: thesis: verum

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

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

then A38: k . 0 = h . (E-max (rectangle (a,b,c,d))) by A20, A37, FUNCT_1:13

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

.= ((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 A35, EUCLID:52

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

s1 in [.0,1.] by A22, A23, XXREAL_1:1;

then A39: k . s1 = h . p1 by A21, A37, FUNCT_1:13

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

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

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

A40: s2 in [.0,1.] by A25, A26, XXREAL_1:1;

then A41: k . s2 = h . p2 by A24, A37, FUNCT_1:13

.= (proj1 . p2) + (proj2 . p2) by A33

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

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

A42: k . 0 >= k . s1 by A2, A7, A38, A39, XREAL_1:7;

A43: k . s1 >= k . s2 by A14, A39, A41, XREAL_1:7;

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

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

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

A46: B is connected by A25, A40, A44, BORSUK_1:40, BORSUK_4:24;

A47: 0 in B by A25, XXREAL_1:1;

A48: s2 in B by A25, XXREAL_1:1;

consider xc being Point of I[01] such that

A49: xc in B and

A50: k . xc = k . s1 by A30, A34, A42, A43, A46, A47, A48, TOPREAL5:5;

reconsider rxc = xc as Real ;

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

x1 = x2

proof

A77:
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

A52: x1 in dom k and

A53: x2 in dom k and

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

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

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

A55: k . x1 = h . (g1 . x1) by A52, FUNCT_1:12

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

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

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

A56: k . x2 = h . (g1 . x2) by A53, FUNCT_1:12

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

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

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

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

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

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

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

end;assume that

A52: x1 in dom k and

A53: x2 in dom k and

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

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

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

A55: k . x1 = h . (g1 . x1) by A52, FUNCT_1:12

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

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

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

A56: k . x2 = h . (g1 . x2) by A53, FUNCT_1:12

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

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

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

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

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

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

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

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 A16, A29, XBOOLE_0:def 3;

end;

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

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

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

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A54, A55, A56, A60, EUCLID:53;

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

hence x1 = x2 by A27, A28, FUNCT_1:def 4; :: thesis: verum

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

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A54, A55, A56, A60, EUCLID:53;

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

hence x1 = x2 by A27, A28, FUNCT_1:def 4; :: thesis: verum

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

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

A63: c <= gr1 `2 by A2, A61, Th1;

A64: gr2 `2 = c by A1, A61, Th3;

A65: gr2 `1 <= b by A1, A61, Th3;

A66: b + (gr1 `2) = (gr2 `1) + c by A2, A54, A55, A56, A61, A64, Th1;

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

hence x1 = x2 by A27, A28, FUNCT_1:def 4; :: thesis: verum

end;A63: c <= gr1 `2 by A2, A61, Th1;

A64: gr2 `2 = c by A1, A61, Th3;

A65: gr2 `1 <= b by A1, A61, Th3;

A66: b + (gr1 `2) = (gr2 `1) + c by A2, A54, A55, A56, A61, A64, Th1;

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

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

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

hence contradiction by A54, A55, A56, A62, A63, A64, XREAL_1:8; :: thesis: verum

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

hence contradiction by A54, A55, A56, A62, A63, A64, XREAL_1:8; :: thesis: verum

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

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

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

hence contradiction by A65, A66, XREAL_1:8; :: thesis: verum

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

hence contradiction by A65, A66, XREAL_1:8; :: thesis: verum

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

hence x1 = x2 by A27, A28, FUNCT_1:def 4; :: thesis: verum

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

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

A70: c <= gr2 `2 by A2, A68, Th1;

A71: gr1 `2 = c by A1, A68, Th3;

A72: gr1 `1 <= b by A1, A68, Th3;

A73: b + (gr2 `2) = (gr1 `1) + c by A1, A54, A55, A56, A68, A69, Th3;

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

hence x1 = x2 by A27, A28, FUNCT_1:def 4; :: thesis: verum

end;A70: c <= gr2 `2 by A2, A68, Th1;

A71: gr1 `2 = c by A1, A68, Th3;

A72: gr1 `1 <= b by A1, A68, Th3;

A73: b + (gr2 `2) = (gr1 `1) + c by A1, A54, A55, A56, A68, A69, Th3;

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

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

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

hence contradiction by A70, A73, XREAL_1:8; :: thesis: verum

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

hence contradiction by A70, A73, XREAL_1:8; :: thesis: verum

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

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

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

hence contradiction by A54, A55, A56, A69, A71, A72, XREAL_1:8; :: thesis: verum

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

hence contradiction by A54, A55, A56, A69, A71, A72, XREAL_1:8; :: thesis: verum

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

hence x1 = x2 by A27, A28, FUNCT_1:def 4; :: thesis: verum

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

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

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

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A54, A55, A56, A76, EUCLID:53;

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

hence x1 = x2 by A27, A28, FUNCT_1:def 4; :: thesis: verum

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

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A54, A55, A56, A76, EUCLID:53;

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

hence x1 = x2 by A27, A28, FUNCT_1:def 4; :: thesis: verum

then s1 in dom k by A22, A23, XXREAL_1:1;

then rxc = s1 by A45, A49, A50, A51, A77;

hence contradiction by A36, A49, XXREAL_1:1; :: thesis: verum

hence LE p1,p2, rectangle (a,b,c,d) by A13, A17, A18, JORDAN6:def 10; :: thesis: verum

case A78:
( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) )
; :: thesis: LE p1,p2, rectangle (a,b,c,d)

then A79:
p2 `2 = c
by A1, Th3;

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

then A81: p2 in Lower_Arc (rectangle (a,b,c,d)) by A78, XBOOLE_0:def 3;

A82: p1 in Lower_Arc (rectangle (a,b,c,d)) by A3, A80, XBOOLE_0:def 3;

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 A78, A81, A82, JORDAN6:def 10; :: thesis: verum

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

then A81: p2 in Lower_Arc (rectangle (a,b,c,d)) by A78, XBOOLE_0:def 3;

A82: p1 in Lower_Arc (rectangle (a,b,c,d)) by A3, A80, XBOOLE_0:def 3;

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

then
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 A81, A82, JORDAN5C:def 3;
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

A83: g is being_homeomorphism and

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

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

A85: g . s1 = p1 and

A86: 0 <= s1 and

A87: s1 <= 1 and

A88: g . s2 = p2 and

A89: 0 <= s2 and

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

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

A92: g is one-to-one by A83, TOPS_2:def 5;

A93: 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 A83, TOPS_2:def 5;

then A94: 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 ;

A95: 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 A96: ( ( 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 A95, 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

A97: 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

A98: h is continuous by A96, JGRAPH_2:19;

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

A99: 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

A83: g is being_homeomorphism and

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

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

A85: g . s1 = p1 and

A86: 0 <= s1 and

A87: s1 <= 1 and

A88: g . s2 = p2 and

A89: 0 <= s2 and

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

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

A92: g is one-to-one by A83, TOPS_2:def 5;

A93: 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 A83, TOPS_2:def 5;

then A94: 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 ;

A95: 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 A96: ( ( 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 A95, 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

A97: 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

A98: h is continuous by A96, JGRAPH_2:19;

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

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

now :: thesis: not s1 > s2

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

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

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

then A102: k . 0 = h . (E-max (rectangle (a,b,c,d))) by A84, A101, FUNCT_1:13

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

.= ((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 A99, EUCLID:52

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

s1 in [.0,1.] by A86, A87, XXREAL_1:1;

then A103: k . s1 = h . p1 by A85, A101, FUNCT_1:13

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

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

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

A104: s2 in [.0,1.] by A89, A90, XXREAL_1:1;

then A105: k . s2 = h . p2 by A88, A101, FUNCT_1:13

.= (proj1 . p2) + (proj2 . p2) by A97

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

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

A106: k . 0 >= k . s1 by A2, A7, A102, A103, XREAL_1:7;

A107: k . s1 >= k . s2 by A12, A103, A105, XREAL_1:7;

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

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

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

A110: B is connected by A89, A104, A108, BORSUK_1:40, BORSUK_4:24;

A111: 0 in B by A89, XXREAL_1:1;

A112: s2 in B by A89, XXREAL_1:1;

consider xc being Point of I[01] such that

A113: xc in B and

A114: k . xc = k . s1 by A94, A98, A106, A107, A110, A111, A112, TOPREAL5:5;

reconsider rxc = xc as Real ;

A115: 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 A86, A87, XXREAL_1:1;

then rxc = s1 by A109, A113, A114, A115, A141;

hence contradiction by A100, A113, XXREAL_1:1; :: thesis: verum

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

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

then A102: k . 0 = h . (E-max (rectangle (a,b,c,d))) by A84, A101, FUNCT_1:13

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

.= ((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 A99, EUCLID:52

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

s1 in [.0,1.] by A86, A87, XXREAL_1:1;

then A103: k . s1 = h . p1 by A85, A101, FUNCT_1:13

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

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

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

A104: s2 in [.0,1.] by A89, A90, XXREAL_1:1;

then A105: k . s2 = h . p2 by A88, A101, FUNCT_1:13

.= (proj1 . p2) + (proj2 . p2) by A97

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

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

A106: k . 0 >= k . s1 by A2, A7, A102, A103, XREAL_1:7;

A107: k . s1 >= k . s2 by A12, A103, A105, XREAL_1:7;

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

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

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

A110: B is connected by A89, A104, A108, BORSUK_1:40, BORSUK_4:24;

A111: 0 in B by A89, XXREAL_1:1;

A112: s2 in B by A89, XXREAL_1:1;

consider xc being Point of I[01] such that

A113: xc in B and

A114: k . xc = k . s1 by A94, A98, A106, A107, A110, A111, A112, TOPREAL5:5;

reconsider rxc = xc as Real ;

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

x1 = x2

proof

A141:
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

A116: x1 in dom k and

A117: x2 in dom k and

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

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

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

A119: k . x1 = h . (g1 . x1) by A116, FUNCT_1:12

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

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

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

A120: k . x2 = h . (g1 . x2) by A117, FUNCT_1:12

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

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

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

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

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

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

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

end;assume that

A116: x1 in dom k and

A117: x2 in dom k and

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

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

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

A119: k . x1 = h . (g1 . x1) by A116, FUNCT_1:12

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

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

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

A120: k . x2 = h . (g1 . x2) by A117, FUNCT_1:12

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

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

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

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

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

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

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

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 A80, A93, XBOOLE_0:def 3;

end;

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

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

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

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A118, A119, A120, A124, EUCLID:53;

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

hence x1 = x2 by A91, A92, FUNCT_1:def 4; :: thesis: verum

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

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A118, A119, A120, A124, EUCLID:53;

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

hence x1 = x2 by A91, A92, FUNCT_1:def 4; :: thesis: verum

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

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

A127: c <= gr1 `2 by A2, A125, Th1;

A128: gr2 `2 = c by A1, A125, Th3;

A129: gr2 `1 <= b by A1, A125, Th3;

A130: b + (gr1 `2) = (gr2 `1) + c by A2, A118, A119, A120, A125, A128, Th1;

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

hence x1 = x2 by A91, A92, FUNCT_1:def 4; :: thesis: verum

end;A127: c <= gr1 `2 by A2, A125, Th1;

A128: gr2 `2 = c by A1, A125, Th3;

A129: gr2 `1 <= b by A1, A125, Th3;

A130: b + (gr1 `2) = (gr2 `1) + c by A2, A118, A119, A120, A125, A128, Th1;

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

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

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

hence contradiction by A118, A119, A120, A126, A127, A128, XREAL_1:8; :: thesis: verum

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

hence contradiction by A118, A119, A120, A126, A127, A128, XREAL_1:8; :: thesis: verum

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

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

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

hence contradiction by A129, A130, XREAL_1:8; :: thesis: verum

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

hence contradiction by A129, A130, XREAL_1:8; :: thesis: verum

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

hence x1 = x2 by A91, A92, FUNCT_1:def 4; :: thesis: verum

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

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

A134: c <= gr2 `2 by A2, A132, Th1;

A135: gr1 `2 = c by A1, A132, Th3;

A136: gr1 `1 <= b by A1, A132, Th3;

A137: b + (gr2 `2) = (gr1 `1) + c by A1, A118, A119, A120, A132, A133, Th3;

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

hence x1 = x2 by A91, A92, FUNCT_1:def 4; :: thesis: verum

end;A134: c <= gr2 `2 by A2, A132, Th1;

A135: gr1 `2 = c by A1, A132, Th3;

A136: gr1 `1 <= b by A1, A132, Th3;

A137: b + (gr2 `2) = (gr1 `1) + c by A1, A118, A119, A120, A132, A133, Th3;

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

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

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

hence contradiction by A134, A137, XREAL_1:8; :: thesis: verum

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

hence contradiction by A134, A137, XREAL_1:8; :: thesis: verum

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

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

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

hence contradiction by A118, A119, A120, A133, A135, A136, XREAL_1:8; :: thesis: verum

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

hence contradiction by A118, A119, A120, A133, A135, A136, XREAL_1:8; :: thesis: verum

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

hence x1 = x2 by A91, A92, FUNCT_1:def 4; :: thesis: verum

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

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

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

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A118, A119, A120, A140, EUCLID:53;

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

hence x1 = x2 by A91, A92, FUNCT_1:def 4; :: thesis: verum

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

then |[(gr1 `1),(gr1 `2)]| = g . r2 by A118, A119, A120, A140, EUCLID:53;

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

hence x1 = x2 by A91, A92, FUNCT_1:def 4; :: thesis: verum

then s1 in dom k by A86, A87, XXREAL_1:1;

then rxc = s1 by A109, A113, A114, A115, A141;

hence contradiction by A100, A113, XXREAL_1:1; :: thesis: verum

hence LE p1,p2, rectangle (a,b,c,d) by A78, A81, A82, JORDAN6:def 10; :: thesis: verum