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