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 object ; :: 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, Th18;
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 object ; :: 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 ;
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; :: thesis: verum