let p1, p2, p3 be Point of (TOP-REAL 2); ( p1,p2,p3 is_a_triangle iff ( p1,p2,p3 are_mutually_different & angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI ) )
hereby ( p1,p2,p3 are_mutually_different & angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI implies p1,p2,p3 is_a_triangle )
assume A1:
p1,
p2,
p3 is_a_triangle
;
( p1,p2,p3 are_mutually_different & angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI )then A2:
not
p2 in LSeg p3,
p1
by Def3;
then A3:
p2 <> p3
by RLTOPSP1:69;
A4:
not
p1 in LSeg p2,
p3
by A1, Def3;
then
(
p1 <> p2 &
p1 <> p3 )
by RLTOPSP1:69;
hence
p1,
p2,
p3 are_mutually_different
by A3, ZFMISC_1:def 5;
( angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI )
not
p3 in LSeg p1,
p2
by A1, Def3;
hence
(
angle p1,
p2,
p3 <> PI &
angle p2,
p3,
p1 <> PI &
angle p3,
p1,
p2 <> PI )
by A4, A2, Th11;
verum
end;
assume A5:
p1,p2,p3 are_mutually_different
; ( not angle p1,p2,p3 <> PI or not angle p2,p3,p1 <> PI or not angle p3,p1,p2 <> PI or p1,p2,p3 is_a_triangle )
then A6:
p1 <> p2
by ZFMISC_1:def 5;
assume A7:
angle p1,p2,p3 <> PI
; ( not angle p2,p3,p1 <> PI or not angle p3,p1,p2 <> PI or p1,p2,p3 is_a_triangle )
A8:
p1 <> p3
by A5, ZFMISC_1:def 5;
A9:
p2 <> p3
by A5, ZFMISC_1:def 5;
assume
angle p2,p3,p1 <> PI
; ( not angle p3,p1,p2 <> PI or p1,p2,p3 is_a_triangle )
then A10:
not p3 in LSeg p2,p1
by A8, A9, Th8;
assume
angle p3,p1,p2 <> PI
; p1,p2,p3 is_a_triangle
then A11:
not p1 in LSeg p3,p2
by A6, A8, Th8;
not p2 in LSeg p1,p3
by A6, A9, A7, Th8;
hence
p1,p2,p3 is_a_triangle
by A10, A11, Def3; verum