theorem :: EUCLID11:7

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) = 0 & angle (C,A,B) = 0 & ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI )