let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) implies ( |(p1,p2)| = 0 iff ( angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) ) )
assume ( p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) ) ; :: thesis: ( |(p1,p2)| = 0 iff ( angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) )
then A1: ( euc2cpx p1 <> 0c & euc2cpx p2 <> 0c ) by Th2, Th16;
|(p1,p2)| = Re ((euc2cpx p1) .|. (euc2cpx p2)) by Th42;
hence ( |(p1,p2)| = 0 iff ( angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) ) by A1, Th17, COMPLEX2:75; :: thesis: verum