let P be non empty compact Subset of (); :: thesis: for q1, q2 being Point of () st P is being_simple_closed_curve & LE q1,q2,P & q1 <> q2 & q1 <> W-min P holds
(Segment (q2,(),P)) /\ (Segment ((),q1,P)) = {()}

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