let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1)
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1) )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1)
then L_Segment (P,p1,p2,q2) = R_Segment (P,p2,p1,q2) by Th28;
hence Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1) by A1, Th28, JORDAN5B:14; :: thesis: verum