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 & q1 in P & q2 in P 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 & q1 in P & q2 in P implies Segment P,p1,p2,q1,q2 = Segment P,p2,p1,q2,q1 )
assume A1: ( P is_an_arc_of p1,p2 & q1 in P & q2 in P ) ; :: 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 Th31;
hence Segment P,p1,p2,q1,q2 = Segment P,p2,p1,q2,q1 by A1, Th31, JORDAN5B:14; :: thesis: verum