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 A1: ( 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 A2: euc2cpx p1 <> 0c by Th2, Th20;
A3: euc2cpx p2 <> 0c by A1, Th2, Th20;
|(p1,p2)| = Re ((euc2cpx p1) .|. (euc2cpx p2)) by Th51;
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 A2, A3, Th21, COMPLEX2:89; :: thesis: verum