let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
L_Segment P,p1,p2,q = R_Segment P,p2,p1,q
let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies L_Segment P,p1,p2,q = R_Segment P,p2,p1,q )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: L_Segment P,p1,p2,q = R_Segment P,p2,p1,q
thus L_Segment P,p1,p2,q c= R_Segment P,p2,p1,q :: according to XBOOLE_0:def 10 :: thesis: R_Segment P,p2,p1,q c= L_Segment P,p1,p2,q

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in L_Segment P,p1,p2,q or x in R_Segment P,p2,p1,q )
assume x in L_Segment P,p1,p2,q ; :: thesis: x in R_Segment P,p2,p1,q
then consider p being Point of (TOP-REAL 2) such that
A2: p = x and
A3: LE p,q,P,p1,p2 ;
LE q,p,P,p2,p1 by A1, A3, Th19;
hence x in R_Segment P,p2,p1,q by A2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in R_Segment P,p2,p1,q or x in L_Segment P,p1,p2,q )
assume x in R_Segment P,p2,p1,q ; :: thesis: x in L_Segment P,p1,p2,q
then consider p being Point of (TOP-REAL 2) such that
A4: p = x and
A5: LE q,p,P,p2,p1 ;
LE p,q,P,p1,p2 by A1, A5, Th19, JORDAN5B:14;
hence x in L_Segment P,p1,p2,q by A4; :: thesis: verum