let z1, z2 be Complex; :: thesis: ( ( z1 <> z2 or z1 - z2 <> 0 ) implies ( Arg (z1 - z2) < PI iff Arg (z2 - z1) >= PI ) )
assume ( z1 <> z2 or z1 - z2 <> 0 ) ; :: thesis: ( Arg (z1 - z2) < PI iff Arg (z2 - z1) >= PI )
then z1 - z2 <> 0c ;
then ( Arg (z1 - z2) < PI iff Arg (- (z1 - z2)) >= PI ) by Th14;
hence ( Arg (z1 - z2) < PI iff Arg (z2 - z1) >= PI ) ; :: thesis: verum