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]|,|[b,d]|) & p2 in LSeg (|[b,c]|,|[b,d]|) holds
( LE p1,p2, rectangle (a,b,c,d) iff p1 `2 >= p2 `2 )
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( a < b & c < d & p1 in LSeg (|[b,c]|,|[b,d]|) & p2 in LSeg (|[b,c]|,|[b,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 (|[b,c]|,|[b,d]|) and
A4: p2 in LSeg (|[b,c]|,|[b,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 = b by A2, A3, Th1;
A7: p1 `2 <= d by A2, A3, Th1;
A8: p2 `1 = b by A2, A4, Th1;
A9: p2 `2 <= d by A2, A4, Th1;
A10: W-min (rectangle (a,b,c,d)) = |[a,c]| by A1, A2, Th46;
A11: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;
A12: Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[b,d]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[a,c]|)) by A1, A2, Th52;
then A13: LSeg (|[b,d]|,|[b,c]|) c= Lower_Arc (rectangle (a,b,c,d)) by XBOOLE_1:7;
A14: (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;
A15: now :: thesis: ( p1 in Upper_Arc (rectangle (a,b,c,d)) implies p1 = E-max (rectangle (a,b,c,d)) )
assume p1 in Upper_Arc (rectangle (a,b,c,d)) ; :: thesis: p1 = E-max (rectangle (a,b,c,d))
then A16: p1 in (Upper_Arc (rectangle (a,b,c,d))) /\ (Lower_Arc (rectangle (a,b,c,d))) by A3, A13, XBOOLE_0:def 4;
now :: thesis: not p1 = W-min (rectangle (a,b,c,d))
assume p1 = W-min (rectangle (a,b,c,d)) ; :: thesis: contradiction
then p1 `1 = a by A10, EUCLID:52;
hence contradiction by A1, A3, TOPREAL3:11; :: thesis: verum
end;
hence p1 = E-max (rectangle (a,b,c,d)) by A14, A16, TARSKI:def 2; :: 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 A17: ( ( 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;
now :: thesis: ( ( p1 = E-max (rectangle (a,b,c,d)) & p1 `2 >= p2 `2 ) or ( p1 <> E-max (rectangle (a,b,c,d)) & p1 `2 >= p2 `2 ) )
per cases ( p1 = E-max (rectangle (a,b,c,d)) or p1 <> E-max (rectangle (a,b,c,d)) ) ;
case p1 = E-max (rectangle (a,b,c,d)) ; :: thesis: p1 `2 >= p2 `2
hence p1 `2 >= p2 `2 by A9, A11, EUCLID:52; :: thesis: verum
end;
case A18: p1 <> E-max (rectangle (a,b,c,d)) ; :: thesis: p1 `2 >= p2 `2
consider f being Function of I[01],((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) such that
A19: f is being_homeomorphism and
A20: f . 0 = E-max (rectangle (a,b,c,d)) and
A21: 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
A22: 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
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, Th54;
reconsider s1 = (((p1 `2) - d) / (c - d)) / 2, s2 = (((p2 `2) - d) / (c - d)) / 2 as Real ;
A23: f . s1 = p1 by A3, A22;
A24: f . s2 = p2 by A4, A22;
d - c > 0 by A2, XREAL_1:50;
then A25: - (d - c) < - 0 by XREAL_1:24;
A26: s1 <= 1 by A3, A22;
A27: 0 <= s2 by A4, A22;
s2 <= 1 by A4, A22;
then s1 <= s2 by A15, A17, A18, A19, A20, A21, A23, A24, A26, A27, JORDAN5C:def 3;
then ((((p1 `2) - d) / (c - d)) / 2) * 2 <= ((((p2 `2) - d) / (c - d)) / 2) * 2 by XREAL_1:64;
then (((p1 `2) - d) / (c - d)) * (c - d) >= (((p2 `2) - d) / (c - d)) * (c - d) by A25, XREAL_1:65;
then (p1 `2) - d >= (((p2 `2) - d) / (c - d)) * (c - d) by A25, XCMPLX_1:87;
then (p1 `2) - d >= (p2 `2) - d by A25, XCMPLX_1:87;
then ((p1 `2) - d) + d >= ((p2 `2) - d) + d by XREAL_1:7;
hence p1 `2 >= p2 `2 ; :: thesis: verum
end;
end;
end;
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 A28: p1 `2 >= p2 `2 ; :: thesis: LE p1,p2, rectangle (a,b,c,d)
now :: thesis: ( ( p2 = W-min (rectangle (a,b,c,d)) & contradiction ) or ( p2 <> W-min (rectangle (a,b,c,d)) & LE p1,p2, 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 A29: p2 <> W-min (rectangle (a,b,c,d)) ; :: thesis: LE p1,p2, rectangle (a,b,c,d)
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
A30: g is being_homeomorphism and
A31: g . 0 = E-max (rectangle (a,b,c,d)) and
g . 1 = W-min (rectangle (a,b,c,d)) and
A32: g . s1 = p1 and
A33: 0 <= s1 and
A34: s1 <= 1 and
A35: g . s2 = p2 and
A36: 0 <= s2 and
A37: s2 <= 1 ; :: thesis: s1 <= s2
A38: dom g = the carrier of I[01] by FUNCT_2:def 1;
A39: g is one-to-one by A30, TOPS_2:def 5;
A40: 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 A30, TOPS_2:def 5;
then A41: 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 ;
A42: 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 A43: ( ( 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 A42, 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
A44: 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
A45: h is continuous by A43, JGRAPH_2:19;
reconsider k = h * g1 as Function of I[01],R^1 ;
A46: E-max (rectangle (a,b,c,d)) = |[b,d]| by A1, A2, Th46;
now :: thesis: not s1 > s2
assume A47: s1 > s2 ; :: thesis: contradiction
A48: dom g = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
0 in [.0,1.] by XXREAL_1:1;
then A49: k . 0 = h . (E-max (rectangle (a,b,c,d))) by A31, A48, FUNCT_1:13
.= (h1 . (E-max (rectangle (a,b,c,d)))) + (h2 . (E-max (rectangle (a,b,c,d)))) by A44
.= ((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
.= b + ((E-max (rectangle (a,b,c,d))) `2) by A46, EUCLID:52
.= b + d by A46, EUCLID:52 ;
s1 in [.0,1.] by A33, A34, XXREAL_1:1;
then A50: k . s1 = h . p1 by A32, A48, FUNCT_1:13
.= (h1 . p1) + (h2 . p1) by A44
.= (p1 `1) + (proj2 . p1) by PSCOMP_1:def 5
.= b + (p1 `2) by A6, PSCOMP_1:def 6 ;
A51: s2 in [.0,1.] by A36, A37, XXREAL_1:1;
then A52: k . s2 = h . p2 by A35, A48, FUNCT_1:13
.= (proj1 . p2) + (proj2 . p2) by A44
.= (p2 `1) + (proj2 . p2) by PSCOMP_1:def 5
.= b + (p2 `2) by A8, PSCOMP_1:def 6 ;
A53: k . 0 >= k . s1 by A7, A49, A50, XREAL_1:7;
A54: k . s1 >= k . s2 by A28, A50, A52, XREAL_1:7;
A55: 0 in [.0,1.] by XXREAL_1:1;
then A56: [.0,s2.] c= [.0,1.] by A51, XXREAL_2:def 12;
reconsider B = [.0,s2.] as Subset of I[01] by A51, A55, BORSUK_1:40, XXREAL_2:def 12;
A57: B is connected by A36, A51, A55, BORSUK_1:40, BORSUK_4:24;
A58: 0 in B by A36, XXREAL_1:1;
A59: s2 in B by A36, XXREAL_1:1;
consider xc being Point of I[01] such that
A60: xc in B and
A61: k . xc = k . s1 by A41, A45, A53, A54, A57, A58, A59, TOPREAL5:5;
reconsider rxc = xc as Real ;
A62: 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
A63: x1 in dom k and
A64: x2 in dom k and
A65: k . x1 = k . x2 ; :: thesis: x1 = x2
reconsider r1 = x1 as Point of I[01] by A63;
reconsider r2 = x2 as Point of I[01] by A64;
A66: k . x1 = h . (g1 . x1) by A63, FUNCT_1:12
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A44
.= ((g1 . r1) `1) + (proj2 . (g1 . r1)) by PSCOMP_1:def 5
.= ((g1 . r1) `1) + ((g1 . r1) `2) by PSCOMP_1:def 6 ;
A67: k . x2 = h . (g1 . x2) by A64, FUNCT_1:12
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A44
.= ((g1 . r2) `1) + (proj2 . (g1 . r2)) by PSCOMP_1:def 5
.= ((g1 . r2) `1) + ((g1 . r2) `2) by PSCOMP_1:def 6 ;
A68: g . r1 in Lower_Arc (rectangle (a,b,c,d)) by A40;
A69: g . r2 in Lower_Arc (rectangle (a,b,c,d)) by A40;
reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A68;
reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A69;
now :: thesis: ( ( g . r1 in LSeg (|[b,c]|,|[b,d]|) & g . r2 in LSeg (|[b,c]|,|[b,d]|) & x1 = x2 ) or ( g . r1 in LSeg (|[b,c]|,|[b,d]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) & x1 = x2 ) or ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[b,d]|) & 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,c]|,|[b,d]|) & g . r2 in LSeg (|[b,c]|,|[b,d]|) ) or ( g . r1 in LSeg (|[b,c]|,|[b,d]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) or ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[b,d]|) ) or ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) ) by A12, A40, XBOOLE_0:def 3;
case A70: ( g . r1 in LSeg (|[b,c]|,|[b,d]|) & g . r2 in LSeg (|[b,c]|,|[b,d]|) ) ; :: thesis: x1 = x2
then A71: gr1 `1 = b by A2, Th1;
gr2 `1 = b by A2, A70, Th1;
then |[(gr1 `1),(gr1 `2)]| = g . r2 by A65, A66, A67, A71, EUCLID:53;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by A38, A39, FUNCT_1:def 4; :: thesis: verum
end;
case A72: ( g . r1 in LSeg (|[b,c]|,|[b,d]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) ; :: thesis: x1 = x2
then A73: gr1 `1 = b by A2, Th1;
A74: c <= gr1 `2 by A2, A72, Th1;
A75: gr2 `2 = c by A1, A72, Th3;
A76: gr2 `1 <= b by A1, A72, Th3;
A77: b + (gr1 `2) = (gr2 `1) + c by A1, A65, A66, A67, A72, A73, Th3;
A78: now :: thesis: not b <> gr2 `1
assume b <> gr2 `1 ; :: thesis: contradiction
then b > gr2 `1 by A76, XXREAL_0:1;
hence contradiction by A74, A77, XREAL_1:8; :: thesis: verum
end;
then |[(gr1 `1),(gr1 `2)]| = g . r2 by A73, A75, A78, EUCLID:53;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by A38, A39, FUNCT_1:def 4; :: thesis: verum
end;
case A79: ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[b,d]|) ) ; :: thesis: x1 = x2
then A80: gr2 `1 = b by A2, Th1;
A81: c <= gr2 `2 by A2, A79, Th1;
A82: gr1 `2 = c by A1, A79, Th3;
A83: gr1 `1 <= b by A1, A79, Th3;
A84: b + (gr2 `2) = (gr1 `1) + c by A1, A65, A66, A67, A79, A80, Th3;
A85: now :: thesis: not b <> gr1 `1
assume b <> gr1 `1 ; :: thesis: contradiction
then b > gr1 `1 by A83, XXREAL_0:1;
hence contradiction by A81, A84, XREAL_1:8; :: thesis: verum
end;
then |[(gr2 `1),(gr2 `2)]| = g . r1 by A80, A82, A85, EUCLID:53;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by A38, A39, FUNCT_1:def 4; :: thesis: verum
end;
case A86: ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) ; :: thesis: x1 = x2
then A87: gr1 `2 = c by A1, Th3;
gr2 `2 = c by A1, A86, Th3;
then |[(gr1 `1),(gr1 `2)]| = g . r2 by A65, A66, A67, A87, EUCLID:53;
then g . r1 = g . r2 by EUCLID:53;
hence x1 = x2 by A38, A39, FUNCT_1:def 4; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
A88: dom k = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then s1 in dom k by A33, A34, XXREAL_1:1;
then rxc = s1 by A56, A60, A61, A62, A88;
hence contradiction by A47, A60, 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 A3, A4, A13, JORDAN5C:def 3;
hence LE p1,p2, rectangle (a,b,c,d) by A3, A4, A13, A29, JORDAN6:def 10; :: thesis: verum
end;
end;
end;
hence LE p1,p2, rectangle (a,b,c,d) ; :: thesis: verum
end;