let P be non empty Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds
(Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3)) = {q2}
let p1, p2, q1, q2, q3 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 implies (Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3)) = {q2} )
assume that
A1: P is_an_arc_of p1,p2 and
A2: LE q1,q2,P,p1,p2 and
A3: LE q2,q3,P,p1,p2 ; :: thesis: (Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3)) = {q2}
A4: q2 in P by A2, JORDAN5C:def 3;
A5: {q2} c= (Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3))

proof

set p3 = q2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {q2} or x in (Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3)) )
assume x in {q2} ; :: thesis: x in (Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3))
then A6: x = q2 by TARSKI:def 1;
LE q2,q2,P,p1,p2 by A4, JORDAN5C:9;
then x in { p31 where p31 is Point of (TOP-REAL 2) : ( LE q2,p31,P,p1,p2 & LE p31,q3,P,p1,p2 ) } by A3, A6;
then A7: x in Segment (P,p1,p2,q2,q3) by JORDAN6:26;
LE q2,q2,P,p1,p2 by A4, JORDAN5C:9;
then x in { p31 where p31 is Point of (TOP-REAL 2) : ( LE q1,p31,P,p1,p2 & LE p31,q2,P,p1,p2 ) } by A2, A6;
then x in Segment (P,p1,p2,q1,q2) by JORDAN6:26;
hence x in (Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3)) by A7, XBOOLE_0:def 4; :: thesis: verum

end;

(Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3)) c= {q2}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3)) or x in {q2} )
assume A8: x in (Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3)) ; :: thesis: x in {q2}
then x in Segment (P,p1,p2,q2,q3) by XBOOLE_0:def 4;
then x in { p4 where p4 is Point of (TOP-REAL 2) : ( LE q2,p4,P,p1,p2 & LE p4,q3,P,p1,p2 ) } by JORDAN6:26;
then A9: ex p4 being Point of (TOP-REAL 2) st
( x = p4 & LE q2,p4,P,p1,p2 & LE p4,q3,P,p1,p2 ) ;
x in Segment (P,p1,p2,q1,q2) by A8, XBOOLE_0:def 4;
then x in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P,p1,p2 & LE p,q2,P,p1,p2 ) } by JORDAN6:26;
then ex p being Point of (TOP-REAL 2) st
( x = p & LE q1,p,P,p1,p2 & LE p,q2,P,p1,p2 ) ;
then x = q2 by A1, A9, JORDAN5C:12;
hence x in {q2} by TARSKI:def 1; :: thesis: verum

end;

hence (Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3)) = {q2} by A5, XBOOLE_0:def 10; :: thesis: verum