let A, B, C, D be Point of (TOP-REAL 2); ( 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
; (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)
;
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;
verum
end;
hence
(angle (B,A,D)) + (angle (D,A,C)) = angle (
B,
A,
C)
by EUCLID_6:4;
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)))
;
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)))
;
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; verum