let A, B, C, D be Point of (TOP-REAL 2); :: thesis: ( 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 implies (angle (A,C,D)) + (angle (D,B,A)) = (2 * PI) - (((angle (B,A,C)) + (angle (A,D,B))) + (angle (C,D,A))) )
assume that
A1: ( 0 < angle (B,A,D) & angle (B,A,D) < PI ) and
A2: ( 0 < angle (D,A,C) & angle (D,A,C) < PI ) and
A3: D,A,C are_mutually_distinct and
A4: B,A,D are_mutually_distinct ; :: thesis: (angle (A,C,D)) + (angle (D,B,A)) = (2 * PI) - (((angle (B,A,C)) + (angle (A,D,B))) + (angle (C,D,A)))
A5: (angle (B,A,D)) + (angle (D,A,C)) = angle (B,A,C)

proof

not (angle (B,A,D)) + (angle (D,A,C)) = (angle (B,A,C)) + (2 * PI)

proof

assume A6: (angle (B,A,D)) + (angle (D,A,C)) = (angle (B,A,C)) + (2 * PI) ; :: thesis: contradiction
0 <= angle (B,A,C) by EUCLID11:2;
then A7: 0 + (2 * PI) <= (angle (B,A,C)) + (2 * PI) by XREAL_1:7;
(angle (B,A,D)) + (angle (D,A,C)) < PI + PI by A1, A2, XREAL_1:8;
hence contradiction by A7, A6; :: thesis: verum

end;

hence (angle (B,A,D)) + (angle (D,A,C)) = angle (B,A,C) by EUCLID_6:4; :: thesis: verum

end;

A8: angle (A,C,D) = PI - ((angle (C,D,A)) + (angle (D,A,C)))

proof

((angle (D,A,C)) + (angle (A,C,D))) + (angle (C,D,A)) = PI by A2, A3, EUCLID_3:47;
hence angle (A,C,D) = PI - ((angle (C,D,A)) + (angle (D,A,C))) ; :: thesis: verum

end;

angle (D,B,A) = PI - ((angle (A,D,B)) + (angle (B,A,D)))

proof

((angle (B,A,D)) + (angle (A,D,B))) + (angle (D,B,A)) = PI by A1, A4, EUCLID_3:47;
hence angle (D,B,A) = PI - ((angle (A,D,B)) + (angle (B,A,D))) ; :: thesis: verum

end;

hence (angle (A,C,D)) + (angle (D,B,A)) = (2 * PI) - (((angle (B,A,C)) + (angle (A,D,B))) + (angle (C,D,A))) by A8, A5; :: thesis: verum