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 ) & q1 <> q3 & ( 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 ) & q1 <> q3 & ( not q2 = q3 or not q2 = W-min P ) implies (Segment q1,q2,P) /\ (Segment q2,q3,P) = {q2} )
assume A1: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & ( not q1 = q2 or not q1 = W-min P ) & q1 <> q3 & ( not q2 = q3 or not q2 = W-min P ) ) ; :: thesis: (Segment q1,q2,P) /\ (Segment q2,q3,P) = {q2}
then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by 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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Segment q1,q2,P) /\ (Segment q2,q3,P) or x in {q2} )
assume x in (Segment q1,q2,P) /\ (Segment q2,q3,P) ; :: thesis: x in {q2}
then A3: ( x in Segment q1,q2,P & x in Segment q2,q3,P ) by XBOOLE_0:def 4;

now

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 A3, Def1;
then consider p being Point of (TOP-REAL 2) such that
A4: ( 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 A3, 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, A4, JORDAN6:72; :: thesis: verum

end;

suppose A5: q2 = W-min P ; :: thesis: x = q2

then ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) by A1, JORDAN6:def 10;
hence x = q2 by A1, A2, A5, JORDAN6:69; :: thesis: verum

end;

end;

end;

case A6: 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 A3, Def1;
then consider p1 being Point of (TOP-REAL 2) such that
A7: ( p1 = x & ( 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 A1, A3, A6, A7, 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, A6, A7, JORDAN6:72; :: thesis: verum

end;

end;

end;

hence x in {q2} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: 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 A8: x = q2 by TARSKI:def 1;
then A9: x in Segment q1,q2,P by A1, Th6;
x in Segment q2,q3,P by A1, A8, Th6;
hence x in (Segment q1,q2,P) /\ (Segment q2,q3,P) by A9, XBOOLE_0:def 4; :: thesis: verum