let A, B, C be Point of (TOP-REAL 2); ( A,B,C are_mutually_distinct & angle (A,B,C) = 0 & not ( angle (B,C,A) = 0 & angle (C,A,B) = PI ) implies ( angle (B,C,A) = PI & angle (C,A,B) = 0 & ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI ) )
assume that
A1:
A,B,C are_mutually_distinct
and
A2:
angle (A,B,C) = 0
; ( ( angle (B,C,A) = 0 & angle (C,A,B) = PI ) or ( angle (B,C,A) = PI & angle (C,A,B) = 0 & ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI ) )
set z1 = euc2cpx A;
set z2 = euc2cpx B;
set z3 = euc2cpx C;
( euc2cpx A <> euc2cpx B & euc2cpx B <> euc2cpx C & euc2cpx A <> euc2cpx C & angle ((euc2cpx A),(euc2cpx B),(euc2cpx C)) = 0 )
by A1, A2, EUCLID_3:4, EUCLID_3:def 4;
per cases then
( ( angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = 0 & angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = PI ) or ( angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = PI & angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = 0 ) )
by COMPLEX2:87;
suppose
(
angle (
(euc2cpx B),
(euc2cpx C),
(euc2cpx A))
= 0 &
angle (
(euc2cpx C),
(euc2cpx A),
(euc2cpx B))
= PI )
;
( ( angle (B,C,A) = 0 & angle (C,A,B) = PI ) or ( angle (B,C,A) = PI & angle (C,A,B) = 0 & ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI ) )hence
( (
angle (
B,
C,
A)
= 0 &
angle (
C,
A,
B)
= PI ) or (
angle (
B,
C,
A)
= PI &
angle (
C,
A,
B)
= 0 &
((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI ) )
by EUCLID_3:def 4;
verum end; suppose
(
angle (
(euc2cpx B),
(euc2cpx C),
(euc2cpx A))
= PI &
angle (
(euc2cpx C),
(euc2cpx A),
(euc2cpx B))
= 0 )
;
( ( angle (B,C,A) = 0 & angle (C,A,B) = PI ) or ( angle (B,C,A) = PI & angle (C,A,B) = 0 & ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI ) )then
(
angle (
B,
C,
A)
= PI &
angle (
C,
A,
B)
= 0 )
by EUCLID_3:def 4;
hence
( (
angle (
B,
C,
A)
= 0 &
angle (
C,
A,
B)
= PI ) or (
angle (
B,
C,
A)
= PI &
angle (
C,
A,
B)
= 0 &
((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI ) )
by A2;
verum end; end;