let P be non empty 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 & 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); :: thesis: ( 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 ; :: thesis: ( LE q1,q2,P,p1,p2 or LE q2,q1,P,p1,p2 )
per cases ( q1 <> q2 or q1 = q2 ) ;
suppose q1 <> q2 ; :: thesis: ( 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; :: thesis: verum
end;
suppose q1 = q2 ; :: thesis: ( 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 A2, JORDAN5C:9; :: thesis: verum
end;
end;