for A, B, C being Point of (TOP-REAL 2) st angle (A,B,C) = 0 & A,B,C are_mutually_distinct & not angle (B,C,A) = PI holds
angle (B,A,C) = PI