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) = Segment P,p1,p2,q1,q3
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) = Segment P,p1,p2,q1,q3 )
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) = Segment P,p1,p2,q1,q3
A4: q2 in P by A2, JORDAN5C:def 3;
A5: Segment P,p1,p2,q1,q3 c= (Segment P,p1,p2,q1,q2) \/ (Segment P,p1,p2,q2,q3)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Segment P,p1,p2,q1,q3 or x in (Segment P,p1,p2,q1,q2) \/ (Segment P,p1,p2,q2,q3) )
assume x in Segment P,p1,p2,q1,q3 ; :: thesis: x in (Segment P,p1,p2,q1,q2) \/ (Segment P,p1,p2,q2,q3)
then x in { p3 where p3 is Point of (TOP-REAL 2) : ( LE q1,p3,P,p1,p2 & LE p3,q3,P,p1,p2 ) } by JORDAN6:29;
then consider p3 being Point of (TOP-REAL 2) such that
A6: x = p3 and
A7: LE q1,p3,P,p1,p2 and
A8: LE p3,q3,P,p1,p2 ;
A9: p3 in P by A7, JORDAN5C:def 3;

now

per cases ( p3 = q2 or p3 <> q2 ) ;

suppose A10: p3 = q2 ; :: thesis: ( x in Segment P,p1,p2,q1,q2 or x in Segment P,p1,p2,q2,q3 )

then LE p3,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, A10;
hence ( x in Segment P,p1,p2,q1,q2 or x in Segment P,p1,p2,q2,q3 ) by JORDAN6:29; :: thesis: verum

end;

suppose A11: p3 <> q2 ; :: thesis: ( x in Segment P,p1,p2,q1,q2 or x in Segment P,p1,p2,q2,q3 )

now

per cases ( ( LE p3,q2,P,p1,p2 & not LE q2,p3,P,p1,p2 ) or ( LE q2,p3,P,p1,p2 & not LE p3,q2,P,p1,p2 ) ) by A1, A4, A9, A11, JORDAN5C:14;

case ( LE p3,q2,P,p1,p2 & not LE q2,p3,P,p1,p2 ) ; :: thesis: ( x in Segment P,p1,p2,q1,q2 or x in Segment P,p1,p2,q2,q3 )

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 A6, A7;
hence ( x in Segment P,p1,p2,q1,q2 or x in Segment P,p1,p2,q2,q3 ) by JORDAN6:29; :: thesis: verum

end;

case ( LE q2,p3,P,p1,p2 & not LE p3,q2,P,p1,p2 ) ; :: thesis: ( x in Segment P,p1,p2,q1,q2 or x in Segment P,p1,p2,q2,q3 )

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 A6, A8;
hence ( x in Segment P,p1,p2,q1,q2 or x in Segment P,p1,p2,q2,q3 ) by JORDAN6:29; :: thesis: verum

end;

end;

end;

hence ( x in Segment P,p1,p2,q1,q2 or x in Segment P,p1,p2,q2,q3 ) ; :: thesis: verum

end;

end;

end;

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

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Segment P,p1,p2,q1,q2) \/ (Segment P,p1,p2,q2,q3) or x in Segment P,p1,p2,q1,q3 )
assume A12: x in (Segment P,p1,p2,q1,q2) \/ (Segment P,p1,p2,q2,q3) ; :: thesis: x in Segment P,p1,p2,q1,q3

per cases ( x in Segment P,p1,p2,q1,q2 or x in Segment P,p1,p2,q2,q3 ) by A12, XBOOLE_0:def 3;

suppose x in Segment P,p1,p2,q1,q2 ; :: thesis: x in Segment P,p1,p2,q1,q3

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:29;
then consider p being Point of (TOP-REAL 2) such that
A13: ( x = p & LE q1,p,P,p1,p2 ) and
A14: LE p,q2,P,p1,p2 ;
LE p,q3,P,p1,p2 by A3, A14, JORDAN5C:13;
then x in { p3 where p3 is Point of (TOP-REAL 2) : ( LE q1,p3,P,p1,p2 & LE p3,q3,P,p1,p2 ) } by A13;
hence x in Segment P,p1,p2,q1,q3 by JORDAN6:29; :: thesis: verum

end;

suppose x in Segment P,p1,p2,q2,q3 ; :: thesis: x in Segment P,p1,p2,q1,q3

then x in { p where p is Point of (TOP-REAL 2) : ( LE q2,p,P,p1,p2 & LE p,q3,P,p1,p2 ) } by JORDAN6:29;
then consider p being Point of (TOP-REAL 2) such that
A15: x = p and
A16: LE q2,p,P,p1,p2 and
A17: LE p,q3,P,p1,p2 ;
LE q1,p,P,p1,p2 by A2, A16, JORDAN5C:13;
then x in { p3 where p3 is Point of (TOP-REAL 2) : ( LE q1,p3,P,p1,p2 & LE p3,q3,P,p1,p2 ) } by A15, A17;
hence x in Segment P,p1,p2,q1,q3 by JORDAN6:29; :: thesis: verum

end;

end;

end;

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