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]|,|[a,d]| holds
( LE p1,p2, rectangle a,b,c,d iff ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| 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 |[a,c]|,|[a,d]| implies ( LE p1,p2, rectangle a,b,c,d iff ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) ) )
set K = rectangle a,b,c,d;
assume A1: ( a < b & c < d & p1 in LSeg |[a,c]|,|[a,d]| ) ; :: thesis: ( LE p1,p2, rectangle a,b,c,d iff ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) )
then A2: rectangle a,b,c,d is being_simple_closed_curve by Th60;
Upper_Arc (rectangle a,b,c,d) = (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) by A1, Th61;
then A3: LSeg |[a,c]|,|[a,d]| c= Upper_Arc (rectangle a,b,c,d) by XBOOLE_1:7;
A4: ( p1 `1 = a & c <= p1 `2 & p1 `2 <= d ) by A1, Th9;
thus ( not LE p1,p2, rectangle a,b,c,d or ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) :: thesis: ( ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| 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 A5: LE p1,p2, rectangle a,b,c,d ; :: thesis: ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) )
then A6: ( p1 in rectangle a,b,c,d & p2 in rectangle a,b,c,d ) by A2, 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 A6, XBOOLE_0:def 3;
then A7: ( 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 A7, XBOOLE_0:def 3;
case p2 in LSeg |[a,c]|,|[a,d]| ; :: thesis: ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) )
hence ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) by A1, A5, Th65; :: thesis: verum
end;
case p2 in LSeg |[a,d]|,|[b,d]| ; :: thesis: ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) )
hence ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) ; :: thesis: verum
end;
case p2 in LSeg |[b,d]|,|[b,c]| ; :: thesis: ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) )
hence ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) ; :: thesis: verum
end;
case A8: p2 in LSeg |[b,c]|,|[a,c]| ; :: thesis: ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| 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 |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| 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 A2, A6, JORDAN7:3;
hence ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) by A1, A5, Th60, JORDAN6:72; :: thesis: verum
end;
case p2 <> W-min (rectangle a,b,c,d) ; :: thesis: ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) )
hence ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) by A8; :: thesis: verum
end;
end;
end;
hence ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| 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 |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) ; :: thesis: verum
end;
A9: W-min (rectangle a,b,c,d) = |[a,c]| by A1, Th56;
thus ( ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| 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 A10: ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| 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 |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) by A10;
case ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) ; :: thesis: LE p1,p2, rectangle a,b,c,d
hence LE p1,p2, rectangle a,b,c,d by A1, Th65; :: thesis: verum
end;
case A11: p2 in LSeg |[a,d]|,|[b,d]| ; :: thesis: LE p1,p2, rectangle a,b,c,d
then A12: ( p2 `2 = d & a <= p2 `1 & p2 `1 <= b ) by A1, Th11;
A13: Upper_Arc (rectangle a,b,c,d) = (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) by A1, Th61;
then A14: p2 in Upper_Arc (rectangle a,b,c,d) by A11, XBOOLE_0:def 3;
A15: p1 in Upper_Arc (rectangle a,b,c,d) by A1, A13, XBOOLE_0:def 3;
LE p1,p2, Upper_Arc (rectangle a,b,c,d), W-min (rectangle a,b,c,d), E-max (rectangle a,b,c,d)
proof
for g being Function of I[01] ,((TOP-REAL 2) | (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[01] ,((TOP-REAL 2) | (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 A16: ( 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 ) ; :: thesis: s1 <= s2
A17: dom g = the carrier of I[01] by FUNCT_2:def 1;
A18: g is one-to-one by A16, TOPS_2:def 5;
A19: the carrier of ((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) = Upper_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 A16, TOPS_2:def 5;
then A20: 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 ;
A21: 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 B24: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ) implies hh1 is continuous ) by JGRAPH_2:39;
A22: now
assume for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ; :: thesis: h1 is continuous
for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh1 . p = proj1 . p ;
hh1 is continuous by B24;
hence h1 is continuous by PRE_TOPC:62; :: thesis: verum
end;
BB: ( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies hh2 is continuous ) by A21, JGRAPH_2:40;
( ( for p being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds hh2 . p = proj2 . p ) implies h2 is continuous ) by BB, PRE_TOPC:62;
then consider h being Function of (TOP-REAL 2),R^1 such that
A23: ( ( 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 ) & h is continuous ) by A22, JGRAPH_2:29;
reconsider k = h * g1 as Function of I[01] ,R^1 ;
A24: k is continuous Function of I[01] ,R^1 by A20, A23;
A25: W-min (rectangle a,b,c,d) = |[a,c]| by A1, Th56;
now
assume A26: s1 > s2 ; :: thesis: contradiction
A27: dom g = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
0 in [.0 ,1.] by XXREAL_1:1;
then A28: k . 0 = h . (W-min (rectangle a,b,c,d)) by A16, A27, FUNCT_1:23
.= (h1 . (W-min (rectangle a,b,c,d))) + (h2 . (W-min (rectangle a,b,c,d))) by A23
.= ((W-min (rectangle a,b,c,d)) `1 ) + (proj2 . (W-min (rectangle a,b,c,d))) by PSCOMP_1:def 28
.= ((W-min (rectangle a,b,c,d)) `1 ) + ((W-min (rectangle a,b,c,d)) `2 ) by PSCOMP_1:def 29
.= ((W-min (rectangle a,b,c,d)) `1 ) + c by A25, EUCLID:56
.= a + c by A25, EUCLID:56 ;
s1 in [.0 ,1.] by A16, XXREAL_1:1;
then A29: k . s1 = h . p1 by A16, A27, FUNCT_1:23
.= (proj1 . p1) + (proj2 . p1) by A23
.= (p1 `1 ) + (proj2 . p1) by PSCOMP_1:def 28
.= a + (p1 `2 ) by A4, PSCOMP_1:def 29 ;
A30: s2 in [.0 ,1.] by A16, XXREAL_1:1;
then k . s2 = h . p2 by A16, A27, FUNCT_1:23
.= (proj1 . p2) + (proj2 . p2) by A23
.= (p2 `1 ) + (proj2 . p2) by PSCOMP_1:def 28
.= (p2 `1 ) + d by A12, PSCOMP_1:def 29 ;
then A31: ( k . 0 <= k . s1 & k . s1 <= k . s2 ) by A4, A12, A28, A29, XREAL_1:9;
A32: 0 in [.0 ,1.] by XXREAL_1:1;
then A33: [.0 ,s2.] c= [.0 ,1.] by A30, XXREAL_2:def 12;
reconsider B = [.0 ,s2.] as Subset of I[01] by A30, A32, BORSUK_1:83, XXREAL_2:def 12;
A34: B is connected by A16, A30, A32, BORSUK_1:83, BORSUK_4:49;
A35: 0 in B by A16, XXREAL_1:1;
A36: s2 in B by A16, XXREAL_1:1;
A37: k . 0 is Real by XREAL_0:def 1;
A38: 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
A39: ( xc in B & k . xc = k . s1 ) by A24, A31, A34, A35, A36, A37, A38, TOPREAL5:11;
xc in [.0 ,1.] by BORSUK_1:83;
then reconsider rxc = xc as Real ;
A40: k is one-to-one
proof
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 A41: ( x1 in dom k & x2 in dom k & k . x1 = k . x2 ) ; :: thesis: x1 = x2
then reconsider r1 = x1 as Point of I[01] ;
reconsider r2 = x2 as Point of I[01] by A41;
A42: k . x1 = h . (g1 . x1) by A41, FUNCT_1:22
.= (h1 . (g1 . r1)) + (h2 . (g1 . r1)) by A23
.= ((g1 . r1) `1 ) + (proj2 . (g1 . r1)) by PSCOMP_1:def 28
.= ((g1 . r1) `1 ) + ((g1 . r1) `2 ) by PSCOMP_1:def 29 ;
A43: k . x2 = h . (g1 . x2) by A41, FUNCT_1:22
.= (h1 . (g1 . r2)) + (h2 . (g1 . r2)) by A23
.= ((g1 . r2) `1 ) + (proj2 . (g1 . r2)) by PSCOMP_1:def 28
.= ((g1 . r2) `1 ) + ((g1 . r2) `2 ) by PSCOMP_1:def 29 ;
A44: g . r1 in Upper_Arc (rectangle a,b,c,d) by A19;
A45: g . r2 in Upper_Arc (rectangle a,b,c,d) by A19;
reconsider gr1 = g . r1 as Point of (TOP-REAL 2) by A44;
reconsider gr2 = g . r2 as Point of (TOP-REAL 2) by A45;
now
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 A13, A19, XBOOLE_0:def 3;
case A46: ( g . r1 in LSeg |[a,c]|,|[a,d]| & g . r2 in LSeg |[a,c]|,|[a,d]| ) ; :: thesis: x1 = x2
then A47: ( gr1 `1 = a & c <= gr1 `2 & gr1 `2 <= d ) by A1, Th9;
( gr2 `1 = a & c <= gr2 `2 & gr2 `2 <= d ) by A1, A46, Th9;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A41, A42, A43, A47, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A17, A18, FUNCT_1:def 8; :: thesis: verum
end;
case A48: ( g . r1 in LSeg |[a,c]|,|[a,d]| & g . r2 in LSeg |[a,d]|,|[b,d]| ) ; :: thesis: x1 = x2
then A49: ( gr1 `1 = a & c <= gr1 `2 & gr1 `2 <= d ) by A1, Th9;
A50: ( gr2 `2 = d & a <= gr2 `1 & gr2 `1 <= b ) by A1, A48, Th11;
A51: a + (gr1 `2 ) = (gr2 `1 ) + d by A1, A41, A42, A43, A48, A49, Th11;
A52: now
assume a <> gr2 `1 ; :: thesis: contradiction
then a < gr2 `1 by A50, XXREAL_0:1;
hence contradiction by A49, A51, XREAL_1:10; :: thesis: verum
end;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A49, A50, A52, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A17, A18, FUNCT_1:def 8; :: thesis: verum
end;
case A53: ( g . r1 in LSeg |[a,d]|,|[b,d]| & g . r2 in LSeg |[a,c]|,|[a,d]| ) ; :: thesis: x1 = x2
then A54: ( gr2 `1 = a & c <= gr2 `2 & gr2 `2 <= d ) by A1, Th9;
A55: ( gr1 `2 = d & a <= gr1 `1 & gr1 `1 <= b ) by A1, A53, Th11;
A56: a + (gr2 `2 ) = (gr1 `1 ) + d by A1, A41, A42, A43, A53, A54, Th11;
A57: now
assume a <> gr1 `1 ; :: thesis: contradiction
then a < gr1 `1 by A55, XXREAL_0:1;
hence contradiction by A54, A56, XREAL_1:10; :: thesis: verum
end;
then |[(gr2 `1 ),(gr2 `2 )]| = g . r1 by A54, A55, A57, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A17, A18, FUNCT_1:def 8; :: thesis: verum
end;
case A58: ( g . r1 in LSeg |[a,d]|,|[b,d]| & g . r2 in LSeg |[a,d]|,|[b,d]| ) ; :: thesis: x1 = x2
then A59: ( gr1 `2 = d & a <= gr1 `1 & gr1 `1 <= b ) by A1, Th11;
( gr2 `2 = d & a <= gr2 `1 & gr2 `1 <= b ) by A1, A58, Th11;
then |[(gr1 `1 ),(gr1 `2 )]| = g . r2 by A41, A42, A43, A59, EUCLID:57;
then g . r1 = g . r2 by EUCLID:57;
hence x1 = x2 by A17, A18, FUNCT_1:def 8; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
hence k is one-to-one by FUNCT_1:def 8; :: thesis: verum
end;
A60: dom k = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then s1 in dom k by A16, XXREAL_1:1;
then rxc = s1 by A33, A39, A40, A60, FUNCT_1:def 8;
hence contradiction by A26, A39, XXREAL_1:1; :: thesis: verum
end;
hence s1 <= s2 ; :: thesis: verum
end;
hence 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 A14, A15, JORDAN5C:def 3; :: thesis: verum
end;
hence LE p1,p2, rectangle a,b,c,d by A14, A15, JORDAN6:def 10; :: thesis: verum
end;
case A64: ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ; :: thesis: LE p1,p2, rectangle a,b,c,d
Lower_Arc (rectangle a,b,c,d) = (LSeg |[b,d]|,|[b,c]|) \/ (LSeg |[b,c]|,|[a,c]|) by A1, Th62;
then LSeg |[b,c]|,|[a,c]| c= Lower_Arc (rectangle a,b,c,d) by XBOOLE_1:7;
hence LE p1,p2, rectangle a,b,c,d by A1, A3, A64, JORDAN6:def 10; :: thesis: verum
end;
end;
end;
hence LE p1,p2, rectangle a,b,c,d ; :: thesis: verum
end;