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))

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

(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 {(W-min P)} or x in (Segment (q2,(W-min P),P)) /\ (Segment ((W-min P),q1,P)) )
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;

end;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 ) )end;

hence
x in {(W-min P)}
by TARSKI:def 1; :: thesis: verumper cases
( LE q2,p1,P or ( q2 in P & p1 = W-min P ) )
by A7;

end;

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;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

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