let P be Subset of ; :: thesis: for p1, p2, q1 being Point of st P is_an_arc_of p1,p2 holds
R_Segment P,p1,p2,q1 = L_Segment P,p2,p1,q1
let p1, p2, q1 be Point of ; :: thesis: ( P is_an_arc_of p1,p2 implies R_Segment P,p1,p2,q1 = L_Segment P,p2,p1,q1 )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: R_Segment P,p1,p2,q1 = L_Segment P,p2,p1,q1
A2: { q where q is Point of : LE q1,q,P,p1,p2 } c= { q2 where q2 is Point of : LE q2,q1,P,p2,p1 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of : LE q1,q,P,p1,p2 } or x in { q2 where q2 is Point of : LE q2,q1,P,p2,p1 } )
assume x in { q where q is Point of : LE q1,q,P,p1,p2 } ; :: thesis: x in { q2 where q2 is Point of : LE q2,q1,P,p2,p1 }
then consider q being Point of such that
A3: q = x and
A4: LE q1,q,P,p1,p2 ;
LE q,q1,P,p2,p1 by A1, A4, Th19;
hence x in { q2 where q2 is Point of : LE q2,q1,P,p2,p1 } by A3; :: thesis: verum

end;

{ q2 where q2 is Point of : LE q2,q1,P,p2,p1 } c= { q where q is Point of : LE q1,q,P,p1,p2 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q2 where q2 is Point of : LE q2,q1,P,p2,p1 } or x in { q where q is Point of : LE q1,q,P,p1,p2 } )
assume x in { q where q is Point of : LE q,q1,P,p2,p1 } ; :: thesis: x in { q where q is Point of : LE q1,q,P,p1,p2 }
then consider q being Point of such that
A5: q = x and
A6: LE q,q1,P,p2,p1 ;
LE q1,q,P,p1,p2 by A1, A6, Th19, JORDAN5B:14;
hence x in { q where q is Point of : LE q1,q,P,p1,p2 } by A5; :: thesis: verum

end;

hence R_Segment P,p1,p2,q1 = L_Segment P,p2,p1,q1 by A2, XBOOLE_0:def 10; :: thesis: verum