let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & ( not q1 = q2 or not q1 = W-min P ) & ( not q2 = q3 or not q2 = W-min P ) holds
(Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2}
let q1, q2, q3 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & ( not q1 = q2 or not q1 = W-min P ) & ( not q2 = q3 or not q2 = W-min P ) implies (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2} )
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: ( not q1 = q2 or not q1 = W-min P ) and
A5: ( not q2 = q3 or not q2 = W-min P ) ; :: thesis: (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2}
A6: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:def 8;
thus (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) c= {q2} :: according to XBOOLE_0:def 10 :: thesis: {q2} c= (Segment (q1,q2,P)) /\ (Segment (q2,q3,P))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) or x in {q2} )
assume A7: x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) ; :: thesis: x in {q2}
then A8: x in Segment (q2,q3,P) by XBOOLE_0:def 4;
A9: x in Segment (q1,q2,P) by A7, XBOOLE_0:def 4;
now :: thesis: ( ( q3 <> W-min P & x = q2 ) or ( q3 = W-min P & x = q2 ) )
per cases ( q3 <> W-min P or q3 = W-min P ) ;
case q3 <> W-min P ; :: thesis: verum
then x in { p where p is Point of (TOP-REAL 2) : ( LE q2,p,P & LE p,q3,P ) } by A8, Def1;
then A10: ex p being Point of (TOP-REAL 2) st
( p = x & LE q2,p,P & LE p,q3,P ) ;
per cases ( q2 <> W-min P or q2 = W-min P ) ;
suppose q2 <> W-min P ; :: thesis: x = q2
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( LE q1,p2,P & LE p2,q2,P ) } by A9, Def1;
then ex p2 being Point of (TOP-REAL 2) st
( p2 = x & LE q1,p2,P & LE p2,q2,P ) ;
hence x = q2 by A1, A10, JORDAN6:57; :: thesis: verum
end;
end;
end;
case A12: q3 = W-min P ; :: thesis: x = q2
then x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE q2,p1,P or ( q2 in P & p1 = W-min P ) ) } by A8, Def1;
then consider p1 being Point of (TOP-REAL 2) such that
A13: p1 = x and
A14: ( LE q2,p1,P or ( q2 in P & p1 = W-min P ) ) ;
p1 in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } by A5, A9, A12, A13, Def1;
then ex p being Point of (TOP-REAL 2) st
( p = p1 & LE q1,p,P & LE p,q2,P ) ;
hence x = q2 by A1, A3, A12, A13, A14, JORDAN6:57; :: thesis: verum
end;
end;
end;
hence x in {q2} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {q2} or x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) )
assume x in {q2} ; :: thesis: x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P))
then x = q2 by TARSKI:def 1;
then ( x in Segment (q1,q2,P) & x in Segment (q2,q3,P) ) by A1, A2, A3, Th6;
hence x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) by XBOOLE_0:def 4; :: thesis: verum