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 object ; :: 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:26;
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 :: thesis: ( x in Segment (P,p1,p2,q1,q2) or x in Segment (P,p1,p2,q2,q3) )

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:26; :: 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 :: thesis: ( ( LE p3,q2,P,p1,p2 & not LE q2,p3,P,p1,p2 & ( x in Segment (P,p1,p2,q1,q2) or x in Segment (P,p1,p2,q2,q3) ) ) or ( LE q2,p3,P,p1,p2 & not LE p3,q2,P,p1,p2 & ( x in Segment (P,p1,p2,q1,q2) or x in Segment (P,p1,p2,q2,q3) ) ) )

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