for p1, p2 being Point of (TOP-REAL 2) st p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) holds
( ( ( not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| & not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = - (|.p1.| * |.p2.|) ) or angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) & ( ( not angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 & not angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) or (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| or (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = - (|.p1.| * |.p2.|) ) )