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