let a, b, c, d be real number ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) 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 (TOP-REAL 2); :: 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, Th60;
A5: p1 `1 = b by A2, A3, Th9;
A6: c <= p1 `2 by A2, A3, Th9;
A7: p1 `2 <= d by A2, A3, Th9;
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 A4, JORDAN7:5;
A10: p2 in rectangle a,b,c,d by A4, A8, 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 A10, XBOOLE_0:def 3;
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
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 A11, XBOOLE_0:def 3;
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, Th69;
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, Th60, JORDAN6:72; :: 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, Th70;
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, Th60, JORDAN6:72; :: 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, Th67; :: 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
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 A4, A9, JORDAN7:3;
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, Th60, JORDAN6:72; :: 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
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 A2, Th9;
W-min (rectangle a,b,c,d) = |[a,c]| by A1, A2, Th56;
then A16: p2 <> W-min (rectangle a,b,c,d) by A1, A15, EUCLID:56;
A17: Lower_Arc (rectangle a,b,c,d) = (LSeg |[b,d]|,|[b,c]|) \/ (LSeg |[b,c]|,|[a,c]|) by A1, A2, Th62;
then A18: p2 in Lower_Arc (rectangle a,b,c,d) by A14, XBOOLE_0:def 3;
A19: p1 in Lower_Arc (rectangle a,b,c,d) by A3, A17, 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
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
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 A20, TOPS_2:def 5;
A30: the carrier of ((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d))) = Lower_Arc (rectangle a,b,c,d) by PRE_TOPC:29;
then reconsider g1 = g as Function of I[01] ,(TOP-REAL 2) by FUNCT_2:9;
g is continuous by A20, TOPS_2:def 5;
then A31: g1 is continuous by PRE_TOPC:56;
reconsider h1 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
reconsider h2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
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 ;
A32: 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:66
.= (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:39;
then A33: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies h1 is continuous ) by PRE_TOPC:62;
( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by A32, JGRAPH_2:40;
then ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by PRE_TOPC:62;
then consider h being Function of (TOP-REAL 2),R^1 such that
A34: for p being Point of (TOP-REAL 2)
for r1, r2 being real number st h1 . p = r1 & h2 . p = r2 holds
h . p = r1 + r2 and
A35: h is continuous by A33, JGRAPH_2:29;
reconsider k = h * g1 as Function of I[01] ,R^1 ;
A36: E-max (rectangle a,b,c,d) = |[b,d]| by A1, A2, Th56;
now
assume A37: s1 > s2 ; :: thesis: contradiction
A38: dom g = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
0 in [.0 ,1.] by XXREAL_1:1;
then A39: k . 0 = h . (E-max (rectangle a,b,c,d)) by A21, A38, FUNCT_1:23
.= (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 28
.= ((E-max (rectangle a,b,c,d)) `1 ) + ((E-max (rectangle a,b,c,d)) `2 ) by PSCOMP_1:def 29
.= ((E-max (rectangle a,b,c,d)) `1 ) + d by A36, EUCLID:56
.= b + d by A36, EUCLID:56 ;
s1 in [.0 ,1.] by A23, A24, XXREAL_1:1;
then A40: k . s1 = h . p1 by A22, A38, FUNCT_1:23
.= (proj1 . p1) + (proj2 . p1) by A34
.= (p1 `1 ) + (proj2 . p1) by PSCOMP_1:def 28
.= b + (p1 `2 ) by A5, PSCOMP_1:def 29 ;
A41: s2 in [.0 ,1.] by A26, A27, XXREAL_1:1;
then A42: k . s2 = h . p2 by A25, A38, FUNCT_1:23
.= (proj1 . p2) + (proj2 . p2) by A34
.= (p2 `1 ) + (proj2 . p2) by PSCOMP_1:def 28
.= b + (p2 `2 ) by A15, PSCOMP_1:def 29 ;
A43: k . 0 >= k . s1 by A7, A39, A40, XREAL_1:9;
A44: k . s1 >= k . s2 by A14, A40, A42, XREAL_1:9;
A45: 0 in [.0 ,1.] by XXREAL_1:1;
then A46: [.0 ,s2.] c= [.0 ,1.] by A41, XXREAL_2:def 12;
reconsider B = [.0 ,s2.] as Subset of I[01] by A41, A45, BORSUK_1:83, XXREAL_2:def 12;
A47: B is connected by A26, A41, A45, BORSUK_1:83, BORSUK_4:49;
A48: 0 in B by A26, XXREAL_1:1;
A49: s2 in B by A26, XXREAL_1:1;
A50: k . 0 is Real by XREAL_0:def 1;
A51: k . s2 is Real by XREAL_0:def 1;
k . s1 is Real by XREAL_0:def 1;
then consider xc being Point of I[01] such that
A52: xc in B and
A53: k . xc = k . s1 by A31, A35, A43, A44, A47, A48, A49, A50, A51, TOPREAL5:11;
xc in [.0 ,1.] by BORSUK_1:83;
then reconsider rxc = xc as Real ;
A54: 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
A55: x1 in dom k and
A56: x2 in dom k and
A57: k . x1 = k . x2 ; :: thesis: x1 = x2
reconsider r1 = x1 as Point of I[01] by A55;
reconsider r2 = x2 as Point of I[01] by A56;
A58: k . x1 = h . (g1 . x1) by A55, FUNCT_1:22
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A34
.= ((g1 . r1) `1 ) + (proj2 . (g1 . r1)) by PSCOMP_1:def 28
.= ((g1 . r1) `1 ) + ((g1 . r1) `2 ) by PSCOMP_1:def 29 ;
A59: k . x2 = h . (g1 . x2) by A56, FUNCT_1:22
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A34
.= ((g1 . r2) `1 ) + (proj2 . (g1 . r2)) by PSCOMP_1:def 28
.= ((g1 . r2) `1 ) + ((g1 . r2) `2 ) by PSCOMP_1:def 29 ;
A60: g . r1 in Lower_Arc (rectangle a,b,c,d) by A30;
A61: g . r2 in Lower_Arc (rectangle a,b,c,d) by A30;
reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A60;
reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A61;
now
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 A17, A30, XBOOLE_0:def 3;
case A62: ( g . r1 in LSeg |[b,d]|,|[b,c]| & g . r2 in LSeg |[b,d]|,|[b,c]| ) ; :: thesis: x1 = x2
then A63: gr1 `1 = b by A2, Th9;
gr2 `1 = b by A2, A62, Th9;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A57, A58, A59, A63, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A28, A29, FUNCT_1:def 8; :: thesis: verum
end;
case A64: ( g . r1 in LSeg |[b,d]|,|[b,c]| & g . r2 in LSeg |[b,c]|,|[a,c]| ) ; :: thesis: x1 = x2
then A65: gr1 `1 = b by A2, Th9;
A66: c <= gr1 `2 by A2, A64, Th9;
A67: gr2 `2 = c by A1, A64, Th11;
A68: gr2 `1 <= b by A1, A64, Th11;
A69: b + (gr1 `2 ) = (gr2 `1 ) + c by A2, A57, A58, A59, A64, A67, Th9;
A70: now
assume b <> gr2 `1 ; :: thesis: contradiction
then b > gr2 `1 by A68, XXREAL_0:1;
hence contradiction by A57, A58, A59, A65, A66, A67, XREAL_1:10; :: thesis: verum
end;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A65, A67, A70, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A28, A29, FUNCT_1:def 8; :: thesis: verum
end;
case A71: ( g . r1 in LSeg |[b,c]|,|[a,c]| & g . r2 in LSeg |[b,d]|,|[b,c]| ) ; :: thesis: x1 = x2
then A72: gr2 `1 = b by A2, Th9;
A73: c <= gr2 `2 by A2, A71, Th9;
A74: gr1 `2 = c by A1, A71, Th11;
A75: gr1 `1 <= b by A1, A71, Th11;
A76: b + (gr2 `2 ) = (gr1 `1 ) + c by A1, A57, A58, A59, A71, A72, Th11;
A77: now
assume b <> gr1 `1 ; :: thesis: contradiction
then b > gr1 `1 by A75, XXREAL_0:1;
hence contradiction by A73, A76, XREAL_1:10; :: thesis: verum
end;
then |[(gr2 `1 ),(gr2 `2 )]| = g . r1 by A72, A74, A77, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A28, A29, FUNCT_1:def 8; :: thesis: verum
end;
case A78: ( g . r1 in LSeg |[b,c]|,|[a,c]| & g . r2 in LSeg |[b,c]|,|[a,c]| ) ; :: thesis: x1 = x2
then A79: gr1 `2 = c by A1, Th11;
gr2 `2 = c by A1, A78, Th11;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A57, A58, A59, A79, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A28, A29, FUNCT_1:def 8; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
A80: dom k = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then s1 in dom k by A23, A24, XXREAL_1:1;
then rxc = s1 by A46, A52, A53, A54, A80;
hence contradiction by A37, A52, 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 A18, A19, JORDAN5C:def 3;
hence LE p1,p2, rectangle a,b,c,d by A16, A18, A19, JORDAN6:def 10; :: thesis: verum
end;
case A81: ( 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 A82: p2 `2 = c by A1, Th11;
A83: p2 `1 <= b by A1, A81, Th11;
A84: Lower_Arc (rectangle a,b,c,d) = (LSeg |[b,d]|,|[b,c]|) \/ (LSeg |[b,c]|,|[a,c]|) by A1, A2, Th62;
then A85: p2 in Lower_Arc (rectangle a,b,c,d) by A81, XBOOLE_0:def 3;
A86: p1 in Lower_Arc (rectangle a,b,c,d) by A3, A84, 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
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
A87: g is being_homeomorphism and
A88: g . 0 = E-max (rectangle a,b,c,d) and
g . 1 = W-min (rectangle a,b,c,d) and
A89: g . s1 = p1 and
A90: 0 <= s1 and
A91: s1 <= 1 and
A92: g . s2 = p2 and
A93: 0 <= s2 and
A94: s2 <= 1 ; :: thesis: s1 <= s2
A95: dom g = the carrier of I[01] by FUNCT_2:def 1;
A96: g is one-to-one by A87, TOPS_2:def 5;
A97: the carrier of ((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d))) = Lower_Arc (rectangle a,b,c,d) by PRE_TOPC:29;
then reconsider g1 = g as Function of I[01] ,(TOP-REAL 2) by FUNCT_2:9;
g is continuous by A87, TOPS_2:def 5;
then A98: g1 is continuous by PRE_TOPC:56;
reconsider h1 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
reconsider h2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
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 ;
A99: 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:66
.= (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:39;
then A100: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies h1 is continuous ) by PRE_TOPC:62;
( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by A99, JGRAPH_2:40;
then ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by PRE_TOPC:62;
then consider h being Function of (TOP-REAL 2),R^1 such that
A101: for p being Point of (TOP-REAL 2)
for r1, r2 being real number st h1 . p = r1 & h2 . p = r2 holds
h . p = r1 + r2 and
A102: h is continuous by A100, JGRAPH_2:29;
reconsider k = h * g1 as Function of I[01] ,R^1 ;
A103: E-max (rectangle a,b,c,d) = |[b,d]| by A1, A2, Th56;
now
assume A104: s1 > s2 ; :: thesis: contradiction
A105: dom g = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
0 in [.0 ,1.] by XXREAL_1:1;
then A106: k . 0 = h . (E-max (rectangle a,b,c,d)) by A88, A105, FUNCT_1:23
.= (h1 . (E-max (rectangle a,b,c,d))) + (h2 . (E-max (rectangle a,b,c,d))) by A101
.= ((E-max (rectangle a,b,c,d)) `1 ) + (proj2 . (E-max (rectangle a,b,c,d))) by PSCOMP_1:def 28
.= ((E-max (rectangle a,b,c,d)) `1 ) + ((E-max (rectangle a,b,c,d)) `2 ) by PSCOMP_1:def 29
.= ((E-max (rectangle a,b,c,d)) `1 ) + d by A103, EUCLID:56
.= b + d by A103, EUCLID:56 ;
s1 in [.0 ,1.] by A90, A91, XXREAL_1:1;
then A107: k . s1 = h . p1 by A89, A105, FUNCT_1:23
.= (proj1 . p1) + (proj2 . p1) by A101
.= (p1 `1 ) + (proj2 . p1) by PSCOMP_1:def 28
.= b + (p1 `2 ) by A5, PSCOMP_1:def 29 ;
A108: s2 in [.0 ,1.] by A93, A94, XXREAL_1:1;
then A109: k . s2 = h . p2 by A92, A105, FUNCT_1:23
.= (proj1 . p2) + (proj2 . p2) by A101
.= (p2 `1 ) + (proj2 . p2) by PSCOMP_1:def 28
.= (p2 `1 ) + c by A82, PSCOMP_1:def 29 ;
A110: k . 0 >= k . s1 by A7, A106, A107, XREAL_1:9;
A111: k . s1 >= k . s2 by A6, A83, A107, A109, XREAL_1:9;
A112: 0 in [.0 ,1.] by XXREAL_1:1;
then A113: [.0 ,s2.] c= [.0 ,1.] by A108, XXREAL_2:def 12;
reconsider B = [.0 ,s2.] as Subset of I[01] by A108, A112, BORSUK_1:83, XXREAL_2:def 12;
A114: B is connected by A93, A108, A112, BORSUK_1:83, BORSUK_4:49;
A115: 0 in B by A93, XXREAL_1:1;
A116: s2 in B by A93, XXREAL_1:1;
A117: k . 0 is Real by XREAL_0:def 1;
A118: k . s2 is Real by XREAL_0:def 1;
k . s1 is Real by XREAL_0:def 1;
then consider xc being Point of I[01] such that
A119: xc in B and
A120: k . xc = k . s1 by A98, A102, A110, A111, A114, A115, A116, A117, A118, TOPREAL5:11;
xc in [.0 ,1.] by BORSUK_1:83;
then reconsider rxc = xc as Real ;
A121: 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
A122: x1 in dom k and
A123: x2 in dom k and
A124: k . x1 = k . x2 ; :: thesis: x1 = x2
reconsider r1 = x1 as Point of I[01] by A122;
reconsider r2 = x2 as Point of I[01] by A123;
A125: k . x1 = h . (g1 . x1) by A122, FUNCT_1:22
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A101
.= ((g1 . r1) `1 ) + (proj2 . (g1 . r1)) by PSCOMP_1:def 28
.= ((g1 . r1) `1 ) + ((g1 . r1) `2 ) by PSCOMP_1:def 29 ;
A126: k . x2 = h . (g1 . x2) by A123, FUNCT_1:22
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A101
.= ((g1 . r2) `1 ) + (proj2 . (g1 . r2)) by PSCOMP_1:def 28
.= ((g1 . r2) `1 ) + ((g1 . r2) `2 ) by PSCOMP_1:def 29 ;
A127: g . r1 in Lower_Arc (rectangle a,b,c,d) by A97;
A128: g . r2 in Lower_Arc (rectangle a,b,c,d) by A97;
reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A127;
reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A128;
now
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 A84, A97, XBOOLE_0:def 3;
case A129: ( g . r1 in LSeg |[b,d]|,|[b,c]| & g . r2 in LSeg |[b,d]|,|[b,c]| ) ; :: thesis: x1 = x2
then A130: gr1 `1 = b by A2, Th9;
gr2 `1 = b by A2, A129, Th9;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A124, A125, A126, A130, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A95, A96, FUNCT_1:def 8; :: thesis: verum
end;
case A131: ( g . r1 in LSeg |[b,d]|,|[b,c]| & g . r2 in LSeg |[b,c]|,|[a,c]| ) ; :: thesis: x1 = x2
then A132: gr1 `1 = b by A2, Th9;
A133: c <= gr1 `2 by A2, A131, Th9;
A134: gr2 `2 = c by A1, A131, Th11;
A135: gr2 `1 <= b by A1, A131, Th11;
A136: b + (gr1 `2 ) = (gr2 `1 ) + c by A2, A124, A125, A126, A131, A134, Th9;
A137: now
assume b <> gr2 `1 ; :: thesis: contradiction
then b > gr2 `1 by A135, XXREAL_0:1;
hence contradiction by A124, A125, A126, A132, A133, A134, XREAL_1:10; :: thesis: verum
end;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A132, A134, A137, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A95, A96, FUNCT_1:def 8; :: thesis: verum
end;
case A138: ( g . r1 in LSeg |[b,c]|,|[a,c]| & g . r2 in LSeg |[b,d]|,|[b,c]| ) ; :: thesis: x1 = x2
then A139: gr2 `1 = b by A2, Th9;
A140: c <= gr2 `2 by A2, A138, Th9;
A141: gr1 `2 = c by A1, A138, Th11;
A142: gr1 `1 <= b by A1, A138, Th11;
A143: b + (gr2 `2 ) = (gr1 `1 ) + c by A1, A124, A125, A126, A138, A139, Th11;
A144: now
assume b <> gr1 `1 ; :: thesis: contradiction
then b > gr1 `1 by A142, XXREAL_0:1;
hence contradiction by A140, A143, XREAL_1:10; :: thesis: verum
end;
then |[(gr2 `1 ),(gr2 `2 )]| = g . r1 by A139, A141, A144, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A95, A96, FUNCT_1:def 8; :: thesis: verum
end;
case A145: ( g . r1 in LSeg |[b,c]|,|[a,c]| & g . r2 in LSeg |[b,c]|,|[a,c]| ) ; :: thesis: x1 = x2
then A146: gr1 `2 = c by A1, Th11;
gr2 `2 = c by A1, A145, Th11;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A124, A125, A126, A146, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A95, A96, FUNCT_1:def 8; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
A147: dom k = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then s1 in dom k by A90, A91, XXREAL_1:1;
then rxc = s1 by A113, A119, A120, A121, A147;
hence contradiction by A104, A119, 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 A85, A86, JORDAN5C:def 3;
hence LE p1,p2, rectangle a,b,c,d by A81, A85, A86, JORDAN6:def 10; :: thesis: verum
end;
end;
end;
hence LE p1,p2, rectangle a,b,c,d ; :: thesis: verum
end;