let P be Subset of (TOP-REAL 2); for p1, p2, q1 being Point of (TOP-REAL 2) 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 (TOP-REAL 2); ( 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
; R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)
A2:
{ q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } c= { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 }
proof
let x be
object ;
TARSKI:def 3 ( not x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } or x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } )
assume
x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 }
;
x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 }
then consider q being
Point of
(TOP-REAL 2) 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 (TOP-REAL 2) : LE q2,q1,P,p2,p1 }
by A3;
verum
end;
{ q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } c= { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 }
proof
let x be
object ;
TARSKI:def 3 ( not x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } or x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } )
assume
x in { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p2,p1 }
;
x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 }
then consider q being
Point of
(TOP-REAL 2) such that A5:
q = x
and A6:
LE q,
q1,
P,
p2,
p1
;
LE q1,
q,
P,
p1,
p2
by A1, A6, Th18, JORDAN5B:14;
hence
x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 }
by A5;
verum
end;
hence
R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)
by A2; verum