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

let p1, p2 be Point of (); :: thesis: ( a < b & c < d & p1 in LSeg (|[a,c]|,|[a,d]|) & p2 in LSeg (|[a,c]|,|[a,d]|) implies ( LE p1,p2, rectangle (a,b,c,d) iff p1 `2 <= p2 `2 ) )
set K = rectangle (a,b,c,d);
assume that
A1: a < b and
A2: c < d and
A3: p1 in LSeg (|[a,c]|,|[a,d]|) and
A4: p2 in LSeg (|[a,c]|,|[a,d]|) ; :: thesis: ( LE p1,p2, rectangle (a,b,c,d) iff p1 `2 <= p2 `2 )
A5: rectangle (a,b,c,d) is being_simple_closed_curve by A1, A2, Th50;
A6: p1 `1 = a by A2, A3, Th1;
A7: c <= p1 `2 by A2, A3, Th1;
A8: p2 `1 = a by A2, A4, Th1;
A9: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;
A10: Upper_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) by A1, A2, Th51;
then A11: LSeg (|[a,c]|,|[a,d]|) c= Upper_Arc (rectangle (a,b,c,d)) by XBOOLE_1:7;
A12: (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 ;
A13: now :: thesis: ( p2 in Lower_Arc (rectangle (a,b,c,d)) implies p2 = W-min (rectangle (a,b,c,d)) )
assume p2 in Lower_Arc (rectangle (a,b,c,d)) ; :: thesis: p2 = W-min (rectangle (a,b,c,d))
then A14: p2 in (Upper_Arc (rectangle (a,b,c,d))) /\ (Lower_Arc (rectangle (a,b,c,d))) by ;
now :: thesis: not p2 = E-max (rectangle (a,b,c,d))
assume p2 = E-max (rectangle (a,b,c,d)) ; :: thesis: contradiction
then p2 `1 = b by ;
hence contradiction by A1, A4, TOPREAL3:11; :: thesis: verum
end;
hence p2 = W-min (rectangle (a,b,c,d)) by ; :: thesis: verum
end;
thus ( LE p1,p2, rectangle (a,b,c,d) implies p1 `2 <= p2 `2 ) :: thesis: ( p1 `2 <= p2 `2 implies LE p1,p2, rectangle (a,b,c,d) )
proof
assume LE p1,p2, rectangle (a,b,c,d) ; :: thesis: p1 `2 <= p2 `2
then A15: ( ( 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 JORDAN6:def 10;
consider f being Function of I,(() | (Upper_Arc (rectangle (a,b,c,d)))) such that
A16: f is being_homeomorphism and
A17: f . 0 = W-min (rectangle (a,b,c,d)) and
A18: f . 1 = E-max (rectangle (a,b,c,d)) and
rng f = Upper_Arc (rectangle (a,b,c,d)) and
for r being Real st r in [.0,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) and
for r being Real st r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) and
A19: for p being Point of () st p in LSeg (|[a,c]|,|[a,d]|) holds
( 0 <= (((p `2) - c) / (d - c)) / 2 & (((p `2) - c) / (d - c)) / 2 <= 1 & f . ((((p `2) - c) / (d - c)) / 2) = p ) and
for p being Point of () st p in LSeg (|[a,d]|,|[b,d]|) holds
( 0 <= ((((p `1) - a) / (b - a)) / 2) + (1 / 2) & ((((p `1) - a) / (b - a)) / 2) + (1 / 2) <= 1 & f . (((((p `1) - a) / (b - a)) / 2) + (1 / 2)) = p ) by A1, A2, Th53;
reconsider s1 = (((p1 `2) - c) / (d - c)) / 2, s2 = (((p2 `2) - c) / (d - c)) / 2 as Real ;
A20: f . s1 = p1 by ;
A21: f . s2 = p2 by ;
A22: d - c > 0 by ;
A23: s1 <= 1 by ;
A24: 0 <= s2 by ;
s2 <= 1 by ;
then s1 <= s2 by ;
then ((((p1 `2) - c) / (d - c)) / 2) * 2 <= ((((p2 `2) - c) / (d - c)) / 2) * 2 by XREAL_1:64;
then (((p1 `2) - c) / (d - c)) * (d - c) <= (((p2 `2) - c) / (d - c)) * (d - c) by ;
then (p1 `2) - c <= (((p2 `2) - c) / (d - c)) * (d - c) by ;
then (p1 `2) - c <= (p2 `2) - c by ;
then ((p1 `2) - c) + c <= ((p2 `2) - c) + c by XREAL_1:7;
hence p1 `2 <= p2 `2 ; :: thesis: verum
end;
thus ( p1 `2 <= p2 `2 implies LE p1,p2, rectangle (a,b,c,d) ) :: thesis: verum
proof
assume A25: p1 `2 <= p2 `2 ; :: thesis: LE p1,p2, rectangle (a,b,c,d)
for g being Function of I,(() | (Upper_Arc (rectangle (a,b,c,d))))
for s1, s2 being Real st g is being_homeomorphism & g . 0 = W-min (rectangle (a,b,c,d)) & g . 1 = E-max (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,(() | (Upper_Arc (rectangle (a,b,c,d)))); :: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = W-min (rectangle (a,b,c,d)) & g . 1 = E-max (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 = W-min (rectangle (a,b,c,d)) & g . 1 = E-max (rectangle (a,b,c,d)) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A26: g is being_homeomorphism and
A27: g . 0 = W-min (rectangle (a,b,c,d)) and
g . 1 = E-max (rectangle (a,b,c,d)) and
A28: g . s1 = p1 and
A29: 0 <= s1 and
A30: s1 <= 1 and
A31: g . s2 = p2 and
A32: 0 <= s2 and
A33: s2 <= 1 ; :: thesis: s1 <= s2
A34: dom g = the carrier of I by FUNCT_2:def 1;
A35: g is one-to-one by ;
A36: the carrier of (() | (Upper_Arc (rectangle (a,b,c,d)))) = Upper_Arc (rectangle (a,b,c,d)) by PRE_TOPC:8;
then reconsider g1 = g as Function of I,() by FUNCT_2:7;
g is continuous by ;
then A37: 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 ;
A38: 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 A39: ( ( 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
A40: for p being Point of ()
for r1, r2 being Real st hh1 . p = r1 & hh2 . p = r2 holds
h . p = r1 + r2 and
A41: h is continuous by ;
reconsider k = h * g1 as Function of I,R^1 ;
A42: W-min (rectangle (a,b,c,d)) = |[a,c]| by A1, A2, Th46;
now :: thesis: not s1 > s2
assume A43: s1 > s2 ; :: thesis: contradiction
A44: dom g = [.0,1.] by ;
0 in [.0,1.] by XXREAL_1:1;
then A45: k . 0 = h . (W-min (rectangle (a,b,c,d))) by
.= (h1 . (W-min (rectangle (a,b,c,d)))) + (h2 . (W-min (rectangle (a,b,c,d)))) by A40
.= ((W-min (rectangle (a,b,c,d))) `1) + (proj2 . (W-min (rectangle (a,b,c,d)))) by PSCOMP_1:def 5
.= ((W-min (rectangle (a,b,c,d))) `1) + ((W-min (rectangle (a,b,c,d))) `2) by PSCOMP_1:def 6
.= a + ((W-min (rectangle (a,b,c,d))) `2) by
.= a + c by ;
s1 in [.0,1.] by ;
then A46: k . s1 = h . p1 by
.= (h1 . p1) + (h2 . p1) by A40
.= (p1 `1) + (proj2 . p1) by PSCOMP_1:def 5
.= a + (p1 `2) by ;
A47: s2 in [.0,1.] by ;
then A48: k . s2 = h . p2 by
.= (h1 . p2) + (h2 . p2) by A40
.= (p2 `1) + (proj2 . p2) by PSCOMP_1:def 5
.= a + (p2 `2) by ;
A49: k . 0 <= k . s1 by ;
A50: k . s1 <= k . s2 by ;
A51: 0 in [.0,1.] by XXREAL_1:1;
then A52: [.0,s2.] c= [.0,1.] by ;
reconsider B = [.0,s2.] as Subset of I by ;
A53: B is connected by ;
A54: 0 in B by ;
A55: s2 in B by ;
consider xc being Point of I such that
A56: xc in B and
A57: k . xc = k . s1 by ;
reconsider rxc = xc as Real ;
A58: 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
A59: x1 in dom k and
A60: x2 in dom k and
A61: k . x1 = k . x2 ; :: thesis: x1 = x2
reconsider r1 = x1 as Point of I by A59;
reconsider r2 = x2 as Point of I by A60;
A62: k . x1 = h . (g1 . x1) by
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A40
.= ((g1 . r1) `1) + (proj2 . (g1 . r1)) by PSCOMP_1:def 5
.= ((g1 . r1) `1) + ((g1 . r1) `2) by PSCOMP_1:def 6 ;
A63: k . x2 = h . (g1 . x2) by
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A40
.= ((g1 . r2) `1) + (proj2 . (g1 . r2)) by PSCOMP_1:def 5
.= ((g1 . r2) `1) + ((g1 . r2) `2) by PSCOMP_1:def 6 ;
A64: g . r1 in Upper_Arc (rectangle (a,b,c,d)) by A36;
A65: g . r2 in Upper_Arc (rectangle (a,b,c,d)) by A36;
reconsider gr1 = g . r1 as Point of () by A64;
reconsider gr2 = g . r2 as Point of () by A65;
now :: thesis: ( ( g . r1 in LSeg (|[a,c]|,|[a,d]|) & g . r2 in LSeg (|[a,c]|,|[a,d]|) & x1 = x2 ) or ( g . r1 in LSeg (|[a,c]|,|[a,d]|) & g . r2 in LSeg (|[a,d]|,|[b,d]|) & x1 = x2 ) or ( g . r1 in LSeg (|[a,d]|,|[b,d]|) & g . r2 in LSeg (|[a,c]|,|[a,d]|) & x1 = x2 ) or ( g . r1 in LSeg (|[a,d]|,|[b,d]|) & g . r2 in LSeg (|[a,d]|,|[b,d]|) & x1 = x2 ) )
per cases ( ( g . r1 in LSeg (|[a,c]|,|[a,d]|) & g . r2 in LSeg (|[a,c]|,|[a,d]|) ) or ( g . r1 in LSeg (|[a,c]|,|[a,d]|) & g . r2 in LSeg (|[a,d]|,|[b,d]|) ) or ( g . r1 in LSeg (|[a,d]|,|[b,d]|) & g . r2 in LSeg (|[a,c]|,|[a,d]|) ) or ( g . r1 in LSeg (|[a,d]|,|[b,d]|) & g . r2 in LSeg (|[a,d]|,|[b,d]|) ) ) by ;
case A66: ( g . r1 in LSeg (|[a,c]|,|[a,d]|) & g . r2 in LSeg (|[a,c]|,|[a,d]|) ) ; :: thesis: x1 = x2
then A67: gr1 `1 = a by ;
gr2 `1 = a by A2, A66, 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 A68: ( g . r1 in LSeg (|[a,c]|,|[a,d]|) & g . r2 in LSeg (|[a,d]|,|[b,d]|) ) ; :: thesis: x1 = x2
then A69: gr1 `1 = a by ;
A70: gr1 `2 <= d by A2, A68, Th1;
A71: gr2 `2 = d by A1, A68, Th3;
A72: a <= gr2 `1 by A1, A68, Th3;
A73: a + (gr1 `2) = (gr2 `1) + d by A1, A61, A62, A63, A68, A69, Th3;
A74: now :: thesis: not a <> gr2 `1
assume a <> gr2 `1 ; :: thesis: contradiction
then a < gr2 `1 by ;
hence contradiction by A70, A73, XREAL_1:8; :: thesis: verum
end;
now :: thesis: not gr1 `2 <> d
assume gr1 `2 <> d ; :: thesis: contradiction
then d > gr1 `2 by ;
hence contradiction by A61, A62, A63, A69, A71, A72, 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 A75: ( g . r1 in LSeg (|[a,d]|,|[b,d]|) & g . r2 in LSeg (|[a,c]|,|[a,d]|) ) ; :: thesis: x1 = x2
then A76: gr2 `1 = a by ;
A77: gr2 `2 <= d by A2, A75, Th1;
A78: gr1 `2 = d by A1, A75, Th3;
A79: a <= gr1 `1 by A1, A75, Th3;
A80: a + (gr2 `2) = (gr1 `1) + d by A1, A61, A62, A63, A75, A76, Th3;
A81: now :: thesis: not a <> gr1 `1
assume a <> gr1 `1 ; :: thesis: contradiction
then a < gr1 `1 by ;
hence contradiction by A77, A80, XREAL_1:8; :: thesis: verum
end;
now :: thesis: not gr2 `2 <> d
assume gr2 `2 <> d ; :: thesis: contradiction
then d > gr2 `2 by ;
hence contradiction by A61, A62, A63, A76, A78, A79, 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 A82: ( g . r1 in LSeg (|[a,d]|,|[b,d]|) & g . r2 in LSeg (|[a,d]|,|[b,d]|) ) ; :: thesis: x1 = x2
then A83: gr1 `2 = d by ;
gr2 `2 = d by A1, A82, 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;
A84: dom k = [.0,1.] by ;
then s1 in dom k by ;
then rxc = s1 by A52, A56, A57, A58, A84;
hence contradiction by A43, A56, XXREAL_1:1; :: thesis: verum
end;
hence s1 <= s2 ; :: thesis: verum
end;
then LE p1,p2, Upper_Arc (rectangle (a,b,c,d)), W-min (rectangle (a,b,c,d)), E-max (rectangle (a,b,c,d)) by ;
hence LE p1,p2, rectangle (a,b,c,d) by ; :: thesis: verum
end;