let a, b, c, d be Real; :: thesis: for p1, p2 being Point of () st a < b & c < d & p1 in LSeg (|[b,d]|,|[b,c]|) holds
( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) )

let p1, p2 be Point of (); :: thesis: ( a < b & c < d & p1 in LSeg (|[b,d]|,|[b,c]|) implies ( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & 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,d]|,|[b,c]|) ; :: thesis: ( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) )
A4: rectangle (a,b,c,d) is being_simple_closed_curve by A1, A2, Th50;
A5: p1 `1 = b by A2, A3, Th1;
A6: c <= p1 `2 by A2, A3, Th1;
A7: p1 `2 <= d by A2, A3, Th1;
thus ( not LE p1,p2, rectangle (a,b,c,d) or ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) :: thesis: ( ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) implies LE p1,p2, rectangle (a,b,c,d) )
proof
assume A8: LE p1,p2, rectangle (a,b,c,d) ; :: thesis: ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )
then A9: p1 in rectangle (a,b,c,d) by ;
A10: p2 in rectangle (a,b,c,d) by ;
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 ;
then A11: ( 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,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) or ( p2 in LSeg (|[a,d]|,|[b,d]|) & ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) or ( p2 in LSeg (|[b,d]|,|[b,c]|) & ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) )
per 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 ;
case p2 in LSeg (|[a,c]|,|[a,d]|) ; :: thesis: ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )
then LE p2,p1, rectangle (a,b,c,d) by A1, A2, A3, Th59;
hence ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) by ; :: thesis: verum
end;
case p2 in LSeg (|[a,d]|,|[b,d]|) ; :: thesis: ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )
then LE p2,p1, rectangle (a,b,c,d) by A1, A2, A3, Th60;
hence ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) by ; :: thesis: verum
end;
case p2 in LSeg (|[b,d]|,|[b,c]|) ; :: thesis: ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )
hence ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) by A1, A2, A3, A8, Th57; :: thesis: verum
end;
case A12: p2 in LSeg (|[b,c]|,|[a,c]|) ; :: thesis: ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )
now :: thesis: ( ( p2 = W-min (rectangle (a,b,c,d)) & ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) or ( p2 <> W-min (rectangle (a,b,c,d)) & ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) )
per cases ( p2 = W-min (rectangle (a,b,c,d)) or p2 <> W-min (rectangle (a,b,c,d)) ) ;
case p2 = W-min (rectangle (a,b,c,d)) ; :: thesis: ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )
then LE p2,p1, rectangle (a,b,c,d) by ;
hence ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) by ; :: thesis: verum
end;
case p2 <> W-min (rectangle (a,b,c,d)) ; :: thesis: ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )
hence ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) by A12; :: thesis: verum
end;
end;
end;
hence ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ; :: thesis: verum
end;
end;
end;
hence ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ; :: thesis: verum
end;
thus ( ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) implies LE p1,p2, rectangle (a,b,c,d) ) :: thesis: verum
proof
assume A13: ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ; :: thesis: LE p1,p2, rectangle (a,b,c,d)
now :: thesis: ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 & 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) ) )
per cases ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) by A13;
case A14: ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) ; :: thesis: LE p1,p2, rectangle (a,b,c,d)
then A15: p2 `1 = b by ;
W-min (rectangle (a,b,c,d)) = |[a,c]| by A1, A2, Th46;
then A16: p2 <> W-min (rectangle (a,b,c,d)) by ;
A17: Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[b,d]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[a,c]|)) by A1, A2, Th52;
then A18: p2 in Lower_Arc (rectangle (a,b,c,d)) by ;
A19: p1 in Lower_Arc (rectangle (a,b,c,d)) by ;
for g being Function of I[01],(() | (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],(() | (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
A20: g is being_homeomorphism and
A21: g . 0 = E-max (rectangle (a,b,c,d)) and
g . 1 = W-min (rectangle (a,b,c,d)) and
A22: g . s1 = p1 and
A23: 0 <= s1 and
A24: s1 <= 1 and
A25: g . s2 = p2 and
A26: 0 <= s2 and
A27: s2 <= 1 ; :: thesis: s1 <= s2
A28: dom g = the carrier of I[01] by FUNCT_2:def 1;
A29: g is one-to-one by ;
A30: the carrier of (() | (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],() by FUNCT_2:7;
g is continuous by ;
then A31: g1 is continuous by PRE_TOPC:26;
reconsider h1 = proj1 as Function of (),R^1 by TOPMETR:17;
reconsider h2 = proj2 as Function of (),R^1 by TOPMETR:17;
reconsider hh1 = h1 as Function of TopStruct(# the carrier of (), the topology of () #),R^1 ;
reconsider hh2 = h2 as Function of TopStruct(# the carrier of (), the topology of () #),R^1 ;
A32: TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of (), the topology of () #) | ([#] TopStruct(# the carrier of (), the topology of () #)) by TSEP_1:3
.= TopStruct(# the carrier of (() | ([#] ())), the topology of (() | ([#] ())) #) by PRE_TOPC:36
.= () | ([#] ()) ;
then ( ( for p being Point of (() | ([#] ())) holds hh1 . p = proj1 . p ) implies hh1 is continuous ) by JGRAPH_2:29;
then A33: ( ( for p being Point of (() | ([#] ())) holds hh1 . p = proj1 . p ) implies h1 is continuous ) by PRE_TOPC:32;
( ( for p being Point of (() | ([#] ())) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by ;
then ( ( for p being Point of (() | ([#] ())) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by PRE_TOPC:32;
then consider h being Function of (),R^1 such that
A34: for p being Point of ()
for r1, r2 being Real st h1 . p = r1 & h2 . p = r2 holds
h . p = r1 + r2 and
A35: h is continuous by ;
reconsider k = h * g1 as Function of I[01],R^1 ;
A36: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;
now :: thesis: not s1 > s2
assume A37: s1 > s2 ; :: thesis: contradiction
A38: dom g = [.0,1.] by ;
0 in [.0,1.] by XXREAL_1:1;
then A39: k . 0 = h . (E-max (rectangle (a,b,c,d))) by
.= (h1 . (E-max (rectangle (a,b,c,d)))) + (h2 . (E-max (rectangle (a,b,c,d)))) by A34
.= ((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
.= b + d by ;
s1 in [.0,1.] by ;
then A40: k . s1 = h . p1 by
.= (proj1 . p1) + (proj2 . p1) by A34
.= (p1 `1) + (proj2 . p1) by PSCOMP_1:def 5
.= b + (p1 `2) by ;
A41: s2 in [.0,1.] by ;
then A42: k . s2 = h . p2 by
.= (proj1 . p2) + (proj2 . p2) by A34
.= (p2 `1) + (proj2 . p2) by PSCOMP_1:def 5
.= b + (p2 `2) by ;
A43: k . 0 >= k . s1 by ;
A44: k . s1 >= k . s2 by ;
A45: 0 in [.0,1.] by XXREAL_1:1;
then A46: [.0,s2.] c= [.0,1.] by ;
reconsider B = [.0,s2.] as Subset of I[01] by ;
A47: B is connected by ;
A48: 0 in B by ;
A49: s2 in B by ;
consider xc being Point of I[01] such that
A50: xc in B and
A51: k . xc = k . s1 by ;
reconsider rxc = xc as Real ;
A52: for x1, x2 being set st x1 in dom k & x2 in dom k & k . x1 = k . x2 holds
x1 = x2
proof
let x1, x2 be set ; :: thesis: ( x1 in dom k & x2 in dom k & k . x1 = k . x2 implies x1 = x2 )
assume that
A53: x1 in dom k and
A54: x2 in dom k and
A55: k . x1 = k . x2 ; :: thesis: x1 = x2
reconsider r1 = x1 as Point of I[01] by A53;
reconsider r2 = x2 as Point of I[01] by A54;
A56: k . x1 = h . (g1 . x1) by
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A34
.= ((g1 . r1) `1) + (proj2 . (g1 . r1)) by PSCOMP_1:def 5
.= ((g1 . r1) `1) + ((g1 . r1) `2) by PSCOMP_1:def 6 ;
A57: k . x2 = h . (g1 . x2) by
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A34
.= ((g1 . r2) `1) + (proj2 . (g1 . r2)) by PSCOMP_1:def 5
.= ((g1 . r2) `1) + ((g1 . r2) `2) by PSCOMP_1:def 6 ;
A58: g . r1 in Lower_Arc (rectangle (a,b,c,d)) by A30;
A59: g . r2 in Lower_Arc (rectangle (a,b,c,d)) by A30;
reconsider gr1 = g . r1 as Point of () by A58;
reconsider gr2 = g . r2 as Point of () by A59;
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 ) )
per 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 ;
case A60: ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) ) ; :: thesis: x1 = x2
then A61: gr1 `1 = b by ;
gr2 `1 = b by A2, A60, Th1;
then |[(gr1 `1),(gr1 `2)]| = g . r2 by ;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by ; :: thesis: verum
end;
case A62: ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) ; :: thesis: x1 = x2
then A63: gr1 `1 = b by ;
A64: c <= gr1 `2 by A2, A62, Th1;
A65: gr2 `2 = c by A1, A62, Th3;
A66: gr2 `1 <= b by A1, A62, Th3;
A67: b + (gr1 `2) = (gr2 `1) + c by A2, A55, A56, A57, A62, A65, Th1;
A68: now :: thesis: not b <> gr2 `1
assume b <> gr2 `1 ; :: thesis: contradiction
then b > gr2 `1 by ;
hence contradiction by A55, A56, A57, A63, A64, A65, XREAL_1:8; :: thesis: verum
end;
now :: thesis: not gr1 `2 <> c
assume gr1 `2 <> c ; :: thesis: contradiction
then c < gr1 `2 by ;
hence contradiction by A66, A67, XREAL_1:8; :: thesis: verum
end;
then |[(gr1 `1),(gr1 `2)]| = g . r2 by ;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by ; :: thesis: verum
end;
case A69: ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) ) ; :: thesis: x1 = x2
then A70: gr2 `1 = b by ;
A71: c <= gr2 `2 by A2, A69, Th1;
A72: gr1 `2 = c by A1, A69, Th3;
A73: gr1 `1 <= b by A1, A69, Th3;
A74: b + (gr2 `2) = (gr1 `1) + c by A1, A55, A56, A57, A69, A70, Th3;
A75: now :: thesis: not b <> gr1 `1
assume b <> gr1 `1 ; :: thesis: contradiction
then b > gr1 `1 by ;
hence contradiction by A71, A74, XREAL_1:8; :: thesis: verum
end;
now :: thesis: not gr2 `2 <> c
assume gr2 `2 <> c ; :: thesis: contradiction
then c < gr2 `2 by ;
hence contradiction by A55, A56, A57, A70, A72, A73, XREAL_1:8; :: thesis: verum
end;
then |[(gr2 `1),(gr2 `2)]| = g . r1 by ;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by ; :: thesis: verum
end;
case A76: ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) ; :: thesis: x1 = x2
then A77: gr1 `2 = c by ;
gr2 `2 = c by A1, A76, Th3;
then |[(gr1 `1),(gr1 `2)]| = g . r2 by ;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by ; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
A78: dom k = [.0,1.] by ;
then s1 in dom k by ;
then rxc = s1 by A46, A50, A51, A52, A78;
hence contradiction by A37, A50, XXREAL_1:1; :: thesis: verum
end;
hence s1 <= s2 ; :: thesis: verum
end;
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 ;
hence LE p1,p2, rectangle (a,b,c,d) by ; :: thesis: verum
end;
case A79: ( 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 A80: p2 `2 = c by ;
A81: p2 `1 <= b by A1, A79, Th3;
A82: Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[b,d]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[a,c]|)) by A1, A2, Th52;
then A83: p2 in Lower_Arc (rectangle (a,b,c,d)) by ;
A84: p1 in Lower_Arc (rectangle (a,b,c,d)) by ;
for g being Function of I[01],(() | (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],(() | (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
A85: g is being_homeomorphism and
A86: g . 0 = E-max (rectangle (a,b,c,d)) and
g . 1 = W-min (rectangle (a,b,c,d)) and
A87: g . s1 = p1 and
A88: 0 <= s1 and
A89: s1 <= 1 and
A90: g . s2 = p2 and
A91: 0 <= s2 and
A92: s2 <= 1 ; :: thesis: s1 <= s2
A93: dom g = the carrier of I[01] by FUNCT_2:def 1;
A94: g is one-to-one by ;
A95: the carrier of (() | (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],() by FUNCT_2:7;
g is continuous by ;
then A96: g1 is continuous by PRE_TOPC:26;
reconsider h1 = proj1 as Function of (),R^1 by TOPMETR:17;
reconsider h2 = proj2 as Function of (),R^1 by TOPMETR:17;
reconsider hh1 = h1 as Function of TopStruct(# the carrier of (), the topology of () #),R^1 ;
reconsider hh2 = h2 as Function of TopStruct(# the carrier of (), the topology of () #),R^1 ;
A97: TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of (), the topology of () #) | ([#] TopStruct(# the carrier of (), the topology of () #)) by TSEP_1:3
.= TopStruct(# the carrier of (() | ([#] ())), the topology of (() | ([#] ())) #) by PRE_TOPC:36
.= () | ([#] ()) ;
then ( ( for p being Point of (() | ([#] ())) holds hh1 . p = proj1 . p ) implies hh1 is continuous ) by JGRAPH_2:29;
then A98: ( ( for p being Point of (() | ([#] ())) holds hh1 . p = proj1 . p ) implies h1 is continuous ) by PRE_TOPC:32;
( ( for p being Point of (() | ([#] ())) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by ;
then ( ( for p being Point of (() | ([#] ())) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by PRE_TOPC:32;
then consider h being Function of (),R^1 such that
A99: for p being Point of ()
for r1, r2 being Real st h1 . p = r1 & h2 . p = r2 holds
h . p = r1 + r2 and
A100: h is continuous by ;
reconsider k = h * g1 as Function of I[01],R^1 ;
A101: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;
now :: thesis: not s1 > s2
assume A102: s1 > s2 ; :: thesis: contradiction
A103: dom g = [.0,1.] by ;
0 in [.0,1.] by XXREAL_1:1;
then A104: k . 0 = h . (E-max (rectangle (a,b,c,d))) by
.= (h1 . (E-max (rectangle (a,b,c,d)))) + (h2 . (E-max (rectangle (a,b,c,d)))) by A99
.= ((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
.= b + d by ;
s1 in [.0,1.] by ;
then A105: k . s1 = h . p1 by
.= (proj1 . p1) + (proj2 . p1) by A99
.= (p1 `1) + (proj2 . p1) by PSCOMP_1:def 5
.= b + (p1 `2) by ;
A106: s2 in [.0,1.] by ;
then A107: k . s2 = h . p2 by
.= (proj1 . p2) + (proj2 . p2) by A99
.= (p2 `1) + (proj2 . p2) by PSCOMP_1:def 5
.= (p2 `1) + c by ;
A108: k . 0 >= k . s1 by ;
A109: k . s1 >= k . s2 by ;
A110: 0 in [.0,1.] by XXREAL_1:1;
then A111: [.0,s2.] c= [.0,1.] by ;
reconsider B = [.0,s2.] as Subset of I[01] by ;
A112: B is connected by ;
A113: 0 in B by ;
A114: s2 in B by ;
consider xc being Point of I[01] such that
A115: xc in B and
A116: k . xc = k . s1 by ;
reconsider rxc = xc as Real ;
A117: for x1, x2 being set st x1 in dom k & x2 in dom k & k . x1 = k . x2 holds
x1 = x2
proof
let x1, x2 be set ; :: thesis: ( x1 in dom k & x2 in dom k & k . x1 = k . x2 implies x1 = x2 )
assume that
A118: x1 in dom k and
A119: x2 in dom k and
A120: k . x1 = k . x2 ; :: thesis: x1 = x2
reconsider r1 = x1 as Point of I[01] by A118;
reconsider r2 = x2 as Point of I[01] by A119;
A121: k . x1 = h . (g1 . x1) by
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A99
.= ((g1 . r1) `1) + (proj2 . (g1 . r1)) by PSCOMP_1:def 5
.= ((g1 . r1) `1) + ((g1 . r1) `2) by PSCOMP_1:def 6 ;
A122: k . x2 = h . (g1 . x2) by
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A99
.= ((g1 . r2) `1) + (proj2 . (g1 . r2)) by PSCOMP_1:def 5
.= ((g1 . r2) `1) + ((g1 . r2) `2) by PSCOMP_1:def 6 ;
A123: g . r1 in Lower_Arc (rectangle (a,b,c,d)) by A95;
A124: g . r2 in Lower_Arc (rectangle (a,b,c,d)) by A95;
reconsider gr1 = g . r1 as Point of () by A123;
reconsider gr2 = g . r2 as Point of () by A124;
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 ) )
per 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 ;
case A125: ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) ) ; :: thesis: x1 = x2
then A126: gr1 `1 = b by ;
gr2 `1 = b by ;
then |[(gr1 `1),(gr1 `2)]| = g . r2 by ;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by ; :: thesis: verum
end;
case A127: ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) ; :: thesis: x1 = x2
then A128: gr1 `1 = b by ;
A129: c <= gr1 `2 by ;
A130: gr2 `2 = c by ;
A131: gr2 `1 <= b by ;
A132: b + (gr1 `2) = (gr2 `1) + c by ;
A133: now :: thesis: not b <> gr2 `1
assume b <> gr2 `1 ; :: thesis: contradiction
then b > gr2 `1 by ;
hence contradiction by A120, A121, A122, A128, A129, A130, XREAL_1:8; :: thesis: verum
end;
now :: thesis: not gr1 `2 <> c
assume gr1 `2 <> c ; :: thesis: contradiction
then c < gr1 `2 by ;
hence contradiction by A131, A132, XREAL_1:8; :: thesis: verum
end;
then |[(gr1 `1),(gr1 `2)]| = g . r2 by ;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by ; :: thesis: verum
end;
case A134: ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) ) ; :: thesis: x1 = x2
then A135: gr2 `1 = b by ;
A136: c <= gr2 `2 by ;
A137: gr1 `2 = c by ;
A138: gr1 `1 <= b by ;
A139: b + (gr2 `2) = (gr1 `1) + c by ;
A140: now :: thesis: not b <> gr1 `1
assume b <> gr1 `1 ; :: thesis: contradiction
then b > gr1 `1 by ;
hence contradiction by A136, A139, XREAL_1:8; :: thesis: verum
end;
now :: thesis: not gr2 `2 <> cend;
then |[(gr2 `1),(gr2 `2)]| = g . r1 by ;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by ; :: thesis: verum
end;
case A141: ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) ; :: thesis: x1 = x2
then A142: gr1 `2 = c by ;
gr2 `2 = c by ;
then |[(gr1 `1),(gr1 `2)]| = g . r2 by ;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by ; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
A143: dom k = [.0,1.] by ;
then s1 in dom k by ;
then rxc = s1 by ;
hence contradiction by A102, A115, XXREAL_1:1; :: thesis: verum
end;
hence s1 <= s2 ; :: thesis: verum
end;
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 ;
hence LE p1,p2, rectangle (a,b,c,d) by ; :: thesis: verum
end;
end;
end;
hence LE p1,p2, rectangle (a,b,c,d) ; :: thesis: verum
end;