let a, b, c, d be Real; :: thesis: for p1, p2 being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st a < b & c < d & p1 in closed_inside_of_rectangle (a,b,c,d) & not p2 in closed_inside_of_rectangle (a,b,c,d) & P is_an_arc_of p1,p2 holds
Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= closed_inside_of_rectangle (a,b,c,d)
let p1, p2 be Point of (TOP-REAL 2); :: thesis: for P being Subset of (TOP-REAL 2) st a < b & c < d & p1 in closed_inside_of_rectangle (a,b,c,d) & not p2 in closed_inside_of_rectangle (a,b,c,d) & P is_an_arc_of p1,p2 holds
Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= closed_inside_of_rectangle (a,b,c,d)
let P be Subset of (TOP-REAL 2); :: thesis: ( a < b & c < d & p1 in closed_inside_of_rectangle (a,b,c,d) & not p2 in closed_inside_of_rectangle (a,b,c,d) & P is_an_arc_of p1,p2 implies Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= closed_inside_of_rectangle (a,b,c,d) )
set R = closed_inside_of_rectangle (a,b,c,d);
set dR = rectangle (a,b,c,d);
set n = First_Point (P,p1,p2,(rectangle (a,b,c,d)));
assume that
A1: a < b and
A2: c < d and
A3: p1 in closed_inside_of_rectangle (a,b,c,d) and
A4: not p2 in closed_inside_of_rectangle (a,b,c,d) and
A5: P is_an_arc_of p1,p2 ; :: thesis: Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= closed_inside_of_rectangle (a,b,c,d)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) or x in closed_inside_of_rectangle (a,b,c,d) )
assume that
A6: x in Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) and
A7: not x in closed_inside_of_rectangle (a,b,c,d) ; :: thesis: contradiction
reconsider x = x as Point of (TOP-REAL 2) by A6;
A8: Fr (closed_inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d) by A1, A2, Th52;
p1 in P by A5, TOPREAL1:1;
then A9: P meets closed_inside_of_rectangle (a,b,c,d) by A3, XBOOLE_0:3;
p2 in P by A5, TOPREAL1:1;
then P \ (closed_inside_of_rectangle (a,b,c,d)) <> {} (TOP-REAL 2) by A4, XBOOLE_0:def 5;
then A10: P meets rectangle (a,b,c,d) by A5, A8, A9, CONNSP_1:22, JORDAN6:10;
A11: P is closed by A5, JORDAN6:11;
then A12: P /\ (rectangle (a,b,c,d)) is closed ;
A13: First_Point (P,p1,p2,(rectangle (a,b,c,d))) in P /\ (rectangle (a,b,c,d)) by A5, A10, A11, JORDAN5C:def 1;
per cases ( x = First_Point (P,p1,p2,(rectangle (a,b,c,d))) or x <> First_Point (P,p1,p2,(rectangle (a,b,c,d))) ) ;
suppose x = First_Point (P,p1,p2,(rectangle (a,b,c,d))) ; :: thesis: contradiction
then A14: x in rectangle (a,b,c,d) by A13, XBOOLE_0:def 4;
rectangle (a,b,c,d) c= closed_inside_of_rectangle (a,b,c,d) by A1, A2, Th45;
hence contradiction by A7, A14; :: thesis: verum
end;
suppose A15: x <> First_Point (P,p1,p2,(rectangle (a,b,c,d))) ; :: thesis: contradiction
reconsider P = P as non empty Subset of (TOP-REAL 2) by A5, TOPREAL1:1;
consider f being Function of I[01],((TOP-REAL 2) | P) such that
A16: f is being_homeomorphism and
A17: f . 0 = p1 and
A18: f . 1 = p2 by A5, TOPREAL1:def 1;
A19: rng f = [#] ((TOP-REAL 2) | P) by A16, TOPS_2:def 5
.= P by PRE_TOPC:def 5 ;
First_Point (P,p1,p2,(rectangle (a,b,c,d))) in P by A13, XBOOLE_0:def 4;
then consider na being object such that
A20: na in dom f and
A21: f . na = First_Point (P,p1,p2,(rectangle (a,b,c,d))) by A19, FUNCT_1:def 3;
reconsider na = na as Real by A20;
A22: 0 <= na by A20, BORSUK_1:43;
A23: na <= 1 by A20, BORSUK_1:43;
A24: Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= P by JORDAN16:2;
then consider xa being object such that
A25: xa in dom f and
A26: f . xa = x by A6, A19, FUNCT_1:def 3;
reconsider xa = xa as Real by A25;
A27: 0 <= xa by A25, BORSUK_1:43;
A28: xa <= 1 by A25, BORSUK_1:43;
A29: Segment (P,p1,p2,p1,x) is_an_arc_of p1,x by A3, A5, A6, A7, A24, JORDAN16:24;
then p1 in Segment (P,p1,p2,p1,x) by TOPREAL1:1;
then A30: Segment (P,p1,p2,p1,x) meets closed_inside_of_rectangle (a,b,c,d) by A3, XBOOLE_0:3;
x in Segment (P,p1,p2,p1,x) by A29, TOPREAL1:1;
then (Segment (P,p1,p2,p1,x)) \ (closed_inside_of_rectangle (a,b,c,d)) <> {} (TOP-REAL 2) by A7, XBOOLE_0:def 5;
then Segment (P,p1,p2,p1,x) meets Fr (closed_inside_of_rectangle (a,b,c,d)) by A29, A30, CONNSP_1:22, JORDAN6:10;
then consider z being object such that
A31: z in Segment (P,p1,p2,p1,x) and
A32: z in rectangle (a,b,c,d) by A8, XBOOLE_0:3;
reconsider z = z as Point of (TOP-REAL 2) by A31;
Segment (P,p1,p2,p1,x) = { p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,x,P,p1,p2 ) } by JORDAN6:26;
then A33: ex zz being Point of (TOP-REAL 2) st
( zz = z & LE p1,zz,P,p1,p2 & LE zz,x,P,p1,p2 ) by A31;
Segment (P,p1,p2,p1,x) c= P by JORDAN16:2;
then consider za being object such that
A34: za in dom f and
A35: f . za = z by A19, A31, FUNCT_1:def 3;
reconsider za = za as Real by A34;
A36: 0 <= za by A34, BORSUK_1:43;
A37: za <= 1 by A34, BORSUK_1:43;
A38: na <= za by A5, A10, A12, A16, A17, A18, A21, A23, A32, A35, A36, JORDAN5C:def 1;
A39: za <= xa by A16, A17, A18, A26, A27, A28, A33, A35, A37, JORDAN5C:def 3;
Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) = { p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p, First_Point (P,p1,p2,(rectangle (a,b,c,d))),P,p1,p2 ) } by JORDAN6:26;
then ex xx being Point of (TOP-REAL 2) st
( xx = x & LE p1,xx,P,p1,p2 & LE xx, First_Point (P,p1,p2,(rectangle (a,b,c,d))),P,p1,p2 ) by A6;
then xa <= na by A16, A17, A18, A21, A22, A23, A26, A28, JORDAN5C:def 3;
then xa < na by A15, A21, A26, XXREAL_0:1;
hence contradiction by A38, A39, XXREAL_0:2; :: thesis: verum
end;
end;