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 |[a,c]|,|[b,c]| & p2 in LSeg |[a,c]|,|[b,c]| holds
( LE p1,p2, rectangle a,b,c,d & p1 <> W-min (rectangle a,b,c,d) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) )
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( a < b & c < d & p1 in LSeg |[a,c]|,|[b,c]| & p2 in LSeg |[a,c]|,|[b,c]| implies ( LE p1,p2, rectangle a,b,c,d & p1 <> W-min (rectangle a,b,c,d) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) ) )
set K = rectangle a,b,c,d;
assume that
A1: a < b and
A2: c < d and
A3: p1 in LSeg |[a,c]|,|[b,c]| and
A4: p2 in LSeg |[a,c]|,|[b,c]| ; :: thesis: ( LE p1,p2, rectangle a,b,c,d & p1 <> W-min (rectangle a,b,c,d) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) )
A5: rectangle a,b,c,d is being_simple_closed_curve by A1, A2, Th60;
A6: p1 `2 = c by A1, A3, Th11;
A7: p1 `1 <= b by A1, A3, Th11;
A8: p2 `2 = c by A1, A4, Th11;
A9: a <= p2 `1 by A1, A4, Th11;
A10: W-min (rectangle a,b,c,d) = |[a,c]| by A1, A2, Th56;
A11: E-max (rectangle a,b,c,d) = |[b,d]| by A1, A2, Th56;
A12: Lower_Arc (rectangle a,b,c,d) = (LSeg |[b,d]|,|[b,c]|) \/ (LSeg |[b,c]|,|[a,c]|) by A1, A2, Th62;
then A13: LSeg |[b,c]|,|[a,c]| c= Lower_Arc (rectangle a,b,c,d) by XBOOLE_1:7;
then A14: p1 in Lower_Arc (rectangle a,b,c,d) by A3;
A15: Lower_Arc (rectangle a,b,c,d) c= rectangle a,b,c,d by A5, JORDAN6:76;
A16: (Upper_Arc (rectangle a,b,c,d)) /\ (Lower_Arc (rectangle a,b,c,d)) = {(W-min (rectangle a,b,c,d)),(E-max (rectangle a,b,c,d))} by A5, JORDAN6:def 9;
A17: now
assume p1 in Upper_Arc (rectangle a,b,c,d) ; :: thesis: p1 = W-min (rectangle a,b,c,d)
then p1 in (Upper_Arc (rectangle a,b,c,d)) /\ (Lower_Arc (rectangle a,b,c,d)) by A3, A13, XBOOLE_0:def 4;
then ( p1 = W-min (rectangle a,b,c,d) or p1 = E-max (rectangle a,b,c,d) ) by A16, TARSKI:def 2;
hence p1 = W-min (rectangle a,b,c,d) by A2, A6, A11, EUCLID:56; :: thesis: verum
end;
thus ( LE p1,p2, rectangle a,b,c,d & p1 <> W-min (rectangle a,b,c,d) implies ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) ) :: thesis: ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) implies ( LE p1,p2, rectangle a,b,c,d & p1 <> W-min (rectangle a,b,c,d) ) )
proof
assume that
A18: LE p1,p2, rectangle a,b,c,d and
A19: p1 <> W-min (rectangle a,b,c,d) ; :: thesis: ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) )
A20: ( ( p1 in Upper_Arc (rectangle a,b,c,d) & p2 in Lower_Arc (rectangle a,b,c,d) & not p2 = W-min (rectangle a,b,c,d) ) or ( p1 in Upper_Arc (rectangle a,b,c,d) & p2 in Upper_Arc (rectangle a,b,c,d) & LE p1,p2, Upper_Arc (rectangle a,b,c,d), W-min (rectangle a,b,c,d), E-max (rectangle a,b,c,d) ) or ( p1 in Lower_Arc (rectangle a,b,c,d) & p2 in Lower_Arc (rectangle a,b,c,d) & not p2 = W-min (rectangle a,b,c,d) & LE p1,p2, Lower_Arc (rectangle a,b,c,d), E-max (rectangle a,b,c,d), W-min (rectangle a,b,c,d) ) ) by A18, JORDAN6:def 10;
consider f being Function of I[01] ,((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d))) such that
A21: f is being_homeomorphism and
A22: f . 0 = E-max (rectangle a,b,c,d) and
A23: f . 1 = W-min (rectangle a,b,c,d) and
rng f = Lower_Arc (rectangle a,b,c,d) and
for r being Real st r in [.0 ,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[b,d]|) + ((2 * r) * |[b,c]|) and
for r being Real st r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[b,c]|) + (((2 * r) - 1) * |[a,c]|) and
for p being Point of (TOP-REAL 2) st p in LSeg |[b,d]|,|[b,c]| holds
( 0 <= (((p `2 ) - d) / (c - d)) / 2 & (((p `2 ) - d) / (c - d)) / 2 <= 1 & f . ((((p `2 ) - d) / (c - d)) / 2) = p ) and
A24: for p being Point of (TOP-REAL 2) st p in LSeg |[b,c]|,|[a,c]| holds
( 0 <= ((((p `1 ) - b) / (a - b)) / 2) + (1 / 2) & ((((p `1 ) - b) / (a - b)) / 2) + (1 / 2) <= 1 & f . (((((p `1 ) - b) / (a - b)) / 2) + (1 / 2)) = p ) by A1, A2, Th64;
reconsider s1 = ((((p1 `1 ) - b) / (a - b)) / 2) + (1 / 2), s2 = ((((p2 `1 ) - b) / (a - b)) / 2) + (1 / 2) as Real ;
A25: f . s1 = p1 by A3, A24;
A26: f . s2 = p2 by A4, A24;
b - a > 0 by A1, XREAL_1:52;
then A27: - (b - a) < - 0 by XREAL_1:26;
A28: s1 <= 1 by A3, A24;
A29: 0 <= s2 by A4, A24;
s2 <= 1 by A4, A24;
then s1 <= s2 by A17, A19, A20, A21, A22, A23, A25, A26, A28, A29, JORDAN5C:def 3;
then (((p1 `1 ) - b) / (a - b)) / 2 <= (((p2 `1 ) - b) / (a - b)) / 2 by XREAL_1:8;
then ((((p1 `1 ) - b) / (a - b)) / 2) * 2 <= ((((p2 `1 ) - b) / (a - b)) / 2) * 2 by XREAL_1:66;
then (((p1 `1 ) - b) / (a - b)) * (a - b) >= (((p2 `1 ) - b) / (a - b)) * (a - b) by A27, XREAL_1:67;
then (p1 `1 ) - b >= (((p2 `1 ) - b) / (a - b)) * (a - b) by A27, XCMPLX_1:88;
then (p1 `1 ) - b >= (p2 `1 ) - b by A27, XCMPLX_1:88;
then ((p1 `1 ) - b) + b >= ((p2 `1 ) - b) + b by XREAL_1:9;
hence p1 `1 >= p2 `1 ; :: thesis: p2 <> W-min (rectangle a,b,c,d)
now
assume A30: p2 = W-min (rectangle a,b,c,d) ; :: thesis: contradiction
then LE p2,p1, rectangle a,b,c,d by A5, A14, A15, JORDAN7:3;
hence contradiction by A1, A2, A18, A19, A30, Th60, JORDAN6:72; :: thesis: verum
end;
hence p2 <> W-min (rectangle a,b,c,d) ; :: thesis: verum
end;
thus ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) implies ( LE p1,p2, rectangle a,b,c,d & p1 <> W-min (rectangle a,b,c,d) ) ) :: thesis: verum
proof
assume that
A31: p1 `1 >= p2 `1 and
A32: p2 <> W-min (rectangle a,b,c,d) ; :: thesis: ( LE p1,p2, rectangle a,b,c,d & p1 <> W-min (rectangle a,b,c,d) )
A33: for g being Function of I[01] ,((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d)))
for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max (rectangle a,b,c,d) & g . 1 = W-min (rectangle a,b,c,d) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
proof
let g be Function of I[01] ,((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d))); :: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max (rectangle a,b,c,d) & g . 1 = W-min (rectangle a,b,c,d) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = E-max (rectangle a,b,c,d) & g . 1 = W-min (rectangle a,b,c,d) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A34: g is being_homeomorphism and
A35: g . 0 = E-max (rectangle a,b,c,d) and
g . 1 = W-min (rectangle a,b,c,d) and
A36: g . s1 = p1 and
A37: 0 <= s1 and
A38: s1 <= 1 and
A39: g . s2 = p2 and
A40: 0 <= s2 and
A41: s2 <= 1 ; :: thesis: s1 <= s2
A42: dom g = the carrier of I[01] by FUNCT_2:def 1;
A43: g is one-to-one by A34, TOPS_2:def 5;
A44: the carrier of ((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d))) = Lower_Arc (rectangle a,b,c,d) by PRE_TOPC:29;
then reconsider g1 = g as Function of I[01] ,(TOP-REAL 2) by FUNCT_2:9;
g is continuous by A34, TOPS_2:def 5;
then A45: 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 ;
A46: TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) | ([#] TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #)) by TSEP_1:3
.= TopStruct(# the carrier of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),the topology of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) #) by PRE_TOPC: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 A47: ( ( 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 A46, 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
A48: 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
A49: h is continuous by A47, JGRAPH_2:29;
reconsider k = h * g1 as Function of I[01] ,R^1 ;
A50: E-max (rectangle a,b,c,d) = |[b,d]| by A1, A2, Th56;
now
assume A51: s1 > s2 ; :: thesis: contradiction
A52: dom g = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
0 in [.0 ,1.] by XXREAL_1:1;
then A53: k . 0 = h . (E-max (rectangle a,b,c,d)) by A35, A52, FUNCT_1:23
.= (h1 . (E-max (rectangle a,b,c,d))) + (h2 . (E-max (rectangle a,b,c,d))) by A48
.= ((E-max (rectangle a,b,c,d)) `1 ) + (proj2 . (E-max (rectangle a,b,c,d))) by PSCOMP_1:def 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 A50, EUCLID:56
.= b + d by A50, EUCLID:56 ;
s1 in [.0 ,1.] by A37, A38, XXREAL_1:1;
then A54: k . s1 = h . p1 by A36, A52, FUNCT_1:23
.= (proj1 . p1) + (proj2 . p1) by A48
.= (p1 `1 ) + (proj2 . p1) by PSCOMP_1:def 28
.= (p1 `1 ) + c by A6, PSCOMP_1:def 29 ;
A55: s2 in [.0 ,1.] by A40, A41, XXREAL_1:1;
then A56: k . s2 = h . p2 by A39, A52, FUNCT_1:23
.= (h1 . p2) + (h2 . p2) by A48
.= (p2 `1 ) + (proj2 . p2) by PSCOMP_1:def 28
.= (p2 `1 ) + c by A8, PSCOMP_1:def 29 ;
A57: k . 0 >= k . s1 by A2, A7, A53, A54, XREAL_1:9;
A58: k . s1 >= k . s2 by A31, A54, A56, XREAL_1:9;
A59: 0 in [.0 ,1.] by XXREAL_1:1;
then A60: [.0 ,s2.] c= [.0 ,1.] by A55, XXREAL_2:def 12;
reconsider B = [.0 ,s2.] as Subset of I[01] by A55, A59, BORSUK_1:83, XXREAL_2:def 12;
A61: B is connected by A40, A55, A59, BORSUK_1:83, BORSUK_4:49;
A62: 0 in B by A40, XXREAL_1:1;
A63: s2 in B by A40, XXREAL_1:1;
A64: k . 0 is Real by XREAL_0:def 1;
A65: 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
A66: xc in B and
A67: k . xc = k . s1 by A45, A49, A57, A58, A61, A62, A63, A64, A65, TOPREAL5:11;
xc in [.0 ,1.] by BORSUK_1:83;
then reconsider rxc = xc as Real ;
A68: 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
A69: x1 in dom k and
A70: x2 in dom k and
A71: k . x1 = k . x2 ; :: thesis: x1 = x2
reconsider r1 = x1 as Point of I[01] by A69;
reconsider r2 = x2 as Point of I[01] by A70;
A72: k . x1 = h . (g1 . x1) by A69, FUNCT_1:22
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A48
.= ((g1 . r1) `1 ) + (proj2 . (g1 . r1)) by PSCOMP_1:def 28
.= ((g1 . r1) `1 ) + ((g1 . r1) `2 ) by PSCOMP_1:def 29 ;
A73: k . x2 = h . (g1 . x2) by A70, FUNCT_1:22
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A48
.= ((g1 . r2) `1 ) + (proj2 . (g1 . r2)) by PSCOMP_1:def 28
.= ((g1 . r2) `1 ) + ((g1 . r2) `2 ) by PSCOMP_1:def 29 ;
A74: g . r1 in Lower_Arc (rectangle a,b,c,d) by A44;
A75: g . r2 in Lower_Arc (rectangle a,b,c,d) by A44;
reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A74;
reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A75;
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 A12, A44, XBOOLE_0:def 3;
case A76: ( g . r1 in LSeg |[b,d]|,|[b,c]| & g . r2 in LSeg |[b,d]|,|[b,c]| ) ; :: thesis: x1 = x2
then A77: gr1 `1 = b by A2, Th9;
gr2 `1 = b by A2, A76, Th9;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A71, A72, A73, A77, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A42, A43, FUNCT_1:def 8; :: thesis: verum
end;
case A78: ( g . r1 in LSeg |[b,d]|,|[b,c]| & g . r2 in LSeg |[b,c]|,|[a,c]| ) ; :: thesis: x1 = x2
then A79: gr1 `1 = b by A2, Th9;
A80: c <= gr1 `2 by A2, A78, Th9;
A81: gr2 `2 = c by A1, A78, Th11;
A82: gr2 `1 <= b by A1, A78, Th11;
A83: b + (gr1 `2 ) = (gr2 `1 ) + c by A1, A71, A72, A73, A78, A79, Th11;
A84: now
assume b <> gr2 `1 ; :: thesis: contradiction
then b > gr2 `1 by A82, XXREAL_0:1;
hence contradiction by A80, A83, XREAL_1:10; :: thesis: verum
end;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A79, A81, A84, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A42, A43, FUNCT_1:def 8; :: thesis: verum
end;
case A85: ( g . r1 in LSeg |[b,c]|,|[a,c]| & g . r2 in LSeg |[b,d]|,|[b,c]| ) ; :: thesis: x1 = x2
then A86: gr2 `1 = b by A2, Th9;
A87: c <= gr2 `2 by A2, A85, Th9;
A88: gr1 `2 = c by A1, A85, Th11;
A89: gr1 `1 <= b by A1, A85, Th11;
A90: b + (gr2 `2 ) = (gr1 `1 ) + c by A1, A71, A72, A73, A85, A86, Th11;
A91: now
assume b <> gr1 `1 ; :: thesis: contradiction
then b > gr1 `1 by A89, XXREAL_0:1;
hence contradiction by A87, A90, XREAL_1:10; :: thesis: verum
end;
then |[(gr2 `1 ),(gr2 `2 )]| = g . r1 by A86, A88, A91, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A42, A43, FUNCT_1:def 8; :: thesis: verum
end;
case A92: ( g . r1 in LSeg |[b,c]|,|[a,c]| & g . r2 in LSeg |[b,c]|,|[a,c]| ) ; :: thesis: x1 = x2
then A93: gr1 `2 = c by A1, Th11;
gr2 `2 = c by A1, A92, Th11;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A71, A72, A73, A93, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A42, A43, FUNCT_1:def 8; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
A94: dom k = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then s1 in dom k by A37, A38, XXREAL_1:1;
then rxc = s1 by A60, A66, A67, A68, A94;
hence contradiction by A51, A66, XXREAL_1:1; :: thesis: verum
end;
hence s1 <= s2 ; :: thesis: verum
end;
A95: now
assume A96: p1 = W-min (rectangle a,b,c,d) ; :: thesis: contradiction
then p1 `1 = a by A10, EUCLID:56;
then p1 `1 = p2 `1 by A9, A31, XXREAL_0:1;
then |[(p1 `1 ),(p1 `2 )]| = p2 by A6, A8, EUCLID:57;
hence contradiction by A32, A96, EUCLID:57; :: thesis: verum
end;
LE p1,p2, Lower_Arc (rectangle a,b,c,d), E-max (rectangle a,b,c,d), W-min (rectangle a,b,c,d) by A3, A4, A13, A33, JORDAN5C:def 3;
hence LE p1,p2, rectangle a,b,c,d by A3, A4, A13, A32, JORDAN6:def 10; :: thesis: p1 <> W-min (rectangle a,b,c,d)
thus p1 <> W-min (rectangle a,b,c,d) by A95; :: thesis: verum
end;