let p1, p2, p3 be Point of (TOP-REAL 2); ( p1,p2,p3 is_a_triangle iff ( p1,p2,p3 are_mutually_distinct & angle (p1,p2,p3) <> PI & angle (p2,p3,p1) <> PI & angle (p3,p1,p2) <> PI ) )
hereby ( p1,p2,p3 are_mutually_distinct & 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_distinct & angle (p1,p2,p3) <> PI & angle (p2,p3,p1) <> PI & angle (p3,p1,p2) <> PI )then A2:
not
p2 in LSeg (
p3,
p1)
by TOPREAL9:67;
then A3:
p2 <> p3
by RLTOPSP1:68;
A4:
not
p1 in LSeg (
p2,
p3)
by A1, TOPREAL9:67;
then
(
p1 <> p2 &
p1 <> p3 )
by RLTOPSP1:68;
hence
p1,
p2,
p3 are_mutually_distinct
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, TOPREAL9:67;
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_distinct
; ( 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, TOPREAL9:67; verum