let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q in P holds
L_Segment P,p1,p2,q = R_Segment P,p2,p1,q
let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & q in P implies L_Segment P,p1,p2,q = R_Segment P,p2,p1,q )
assume A1:
( P is_an_arc_of p1,p2 & q in P )
; :: thesis: L_Segment P,p1,p2,q = R_Segment P,p2,p1,q
thus
L_Segment P,p1,p2,q c= R_Segment P,p2,p1,q
:: according to XBOOLE_0:def 10 :: thesis: R_Segment P,p2,p1,q c= L_Segment P,p1,p2,qproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in L_Segment P,p1,p2,q or x in R_Segment P,p2,p1,q )
assume
x in L_Segment P,
p1,
p2,
q
;
:: thesis: x in R_Segment P,p2,p1,q
then consider p being
Point of
(TOP-REAL 2) such that A2:
(
p = x &
LE p,
q,
P,
p1,
p2 )
;
LE q,
p,
P,
p2,
p1
by A1, A2, Th19;
hence
x in R_Segment P,
p2,
p1,
q
by A2;
:: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in R_Segment P,p2,p1,q or x in L_Segment P,p1,p2,q )
assume
x in R_Segment P,p2,p1,q
; :: thesis: x in L_Segment P,p1,p2,q
then consider p being Point of (TOP-REAL 2) such that
A3:
( p = x & LE q,p,P,p2,p1 )
;
LE p,q,P,p1,p2
by A1, A3, Th19, JORDAN5B:14;
hence
x in L_Segment P,p1,p2,q
by A3; :: thesis: verum