let P be non empty Subset of (TOP-REAL 2); 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 & not LE q1,q2,P,p1,p2 holds
LE q2,q1,P,p1,p2
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ( P is_an_arc_of p1,p2 & q1 in P & q2 in P & not LE q1,q2,P,p1,p2 implies LE q2,q1,P,p1,p2 )
assume that
A1:
P is_an_arc_of p1,p2
and
A2:
q1 in P
and
A3:
q2 in P
; ( LE q1,q2,P,p1,p2 or LE q2,q1,P,p1,p2 )
per cases
( q1 <> q2 or q1 = q2 )
;
suppose
q1 <> q2
;
( LE q1,q2,P,p1,p2 or LE q2,q1,P,p1,p2 )hence
(
LE q1,
q2,
P,
p1,
p2 or
LE q2,
q1,
P,
p1,
p2 )
by A1, A2, A3, JORDAN5C:14;
verum end; suppose
q1 = q2
;
( LE q1,q2,P,p1,p2 or LE q2,q1,P,p1,p2 )end; end;