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