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