let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( ( p1 <> p2 or p1 - p2 <> 0. (TOP-REAL 2) ) implies ( Arg (p1 - p2) < PI iff Arg (p2 - p1) >= PI ) )
assume ( p1 <> p2 or p1 - p2 <> 0. (TOP-REAL 2) ) ; :: thesis: ( Arg (p1 - p2) < PI iff Arg (p2 - p1) >= PI )
then A1: p1 - p2 <> 0. (TOP-REAL 2) by RLVECT_1:21;
- (p1 - p2) = p2 - p1 by RLVECT_1:33;
hence ( Arg (p1 - p2) < PI iff Arg (p2 - p1) >= PI ) by A1, Th31; :: thesis: verum