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 ) & ( 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 ) & ( not q2 = q3 or not q2 = W-min P ) implies (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2} )

assume that

A1: P is being_simple_closed_curve and

A2: LE q1,q2,P and

A3: LE q2,q3,P and

A4: ( not q1 = q2 or not q1 = W-min P ) and

A5: ( not q2 = q3 or not q2 = W-min P ) ; :: thesis: (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2}

A6: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, 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))

assume x in {q2} ; :: thesis: x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P))

then x = q2 by TARSKI:def 1;

then ( x in Segment (q1,q2,P) & x in Segment (q2,q3,P) ) by A1, A2, A3, Th6;

hence x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) by XBOOLE_0:def 4; :: thesis: verum

(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 ) & ( not q2 = q3 or not q2 = W-min P ) implies (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2} )

assume that

A1: P is being_simple_closed_curve and

A2: LE q1,q2,P and

A3: LE q2,q3,P and

A4: ( not q1 = q2 or not q1 = W-min P ) and

A5: ( not q2 = q3 or not q2 = W-min P ) ; :: thesis: (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2}

A6: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in {q2} or x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) or x in {q2} )

assume A7: x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) ; :: thesis: x in {q2}

then A8: x in Segment (q2,q3,P) by XBOOLE_0:def 4;

A9: x in Segment (q1,q2,P) by A7, XBOOLE_0:def 4;

end;assume A7: x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) ; :: thesis: x in {q2}

then A8: x in Segment (q2,q3,P) by XBOOLE_0:def 4;

A9: x in Segment (q1,q2,P) by A7, XBOOLE_0:def 4;

now :: thesis: ( ( q3 <> W-min P & x = q2 ) or ( q3 = W-min P & x = q2 ) )end;

hence
x in {q2}
by TARSKI:def 1; :: thesis: verumper cases
( q3 <> W-min P or q3 = W-min P )
;

end;

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 A8, Def1;

then A10: ex p being Point of (TOP-REAL 2) st

( p = x & LE q2,p,P & LE p,q3,P ) ;

end;then A10: ex p being Point of (TOP-REAL 2) st

( p = x & LE q2,p,P & LE p,q3,P ) ;

per cases
( q2 <> W-min P or q2 = W-min P )
;

end;

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 A9, 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, A10, JORDAN6:57; :: thesis: verum

end;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, A10, JORDAN6:57; :: thesis: verum

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

then
LE q1,q2, Upper_Arc P, W-min P, E-max P
by A2, JORDAN6:def 10;

hence x = q2 by A4, A6, A11, JORDAN6:54; :: thesis: verum

end;hence x = q2 by A4, A6, A11, JORDAN6:54; :: thesis: verum

case A12:
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 A8, Def1;

then consider p1 being Point of (TOP-REAL 2) such that

A13: p1 = x and

A14: ( 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 A5, A9, A12, A13, 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, A3, A12, A13, A14, JORDAN6:57; :: thesis: verum

end;then consider p1 being Point of (TOP-REAL 2) such that

A13: p1 = x and

A14: ( 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 A5, A9, A12, A13, 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, A3, A12, A13, A14, JORDAN6:57; :: thesis: verum

assume x in {q2} ; :: thesis: x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P))

then x = q2 by TARSKI:def 1;

then ( x in Segment (q1,q2,P) & x in Segment (q2,q3,P) ) by A1, A2, A3, Th6;

hence x in (Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) by XBOOLE_0:def 4; :: thesis: verum