theorem :: EUCLID11:8

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