let p1, p2, p3, p be Point of (TOP-REAL 2); ( p2 - p1,p3 - p1 are_lindependent2 implies ( p in outside_of_triangle p1,p2,p3 iff ( tricord1 p1,p2,p3,p < 0 or tricord2 p1,p2,p3,p < 0 or tricord3 p1,p2,p3,p < 0 ) ) )
set i1 = tricord1 p1,p2,p3,p;
set i2 = tricord2 p1,p2,p3,p;
set i3 = tricord3 p1,p2,p3,p;
assume A1:
p2 - p1,p3 - p1 are_lindependent2
; ( p in outside_of_triangle p1,p2,p3 iff ( tricord1 p1,p2,p3,p < 0 or tricord2 p1,p2,p3,p < 0 or tricord3 p1,p2,p3,p < 0 ) )
thus
( not p in outside_of_triangle p1,p2,p3 or tricord1 p1,p2,p3,p < 0 or tricord2 p1,p2,p3,p < 0 or tricord3 p1,p2,p3,p < 0 )
( ( tricord1 p1,p2,p3,p < 0 or tricord2 p1,p2,p3,p < 0 or tricord3 p1,p2,p3,p < 0 ) implies p in outside_of_triangle p1,p2,p3 )proof
p in the
carrier of
(TOP-REAL 2)
;
then
p in REAL 2
by EUCLID:25;
then A2:
p in plane p1,
p2,
p3
by A1, Th63;
assume
p in outside_of_triangle p1,
p2,
p3
;
( tricord1 p1,p2,p3,p < 0 or tricord2 p1,p2,p3,p < 0 or tricord3 p1,p2,p3,p < 0 )
then
ex
p0 being
Point of
(TOP-REAL 2) st
(
p0 = p & ex
a1,
a2,
a3 being
Real st
( (
0 > a1 or
0 > a2 or
0 > a3 ) &
(a1 + a2) + a3 = 1 &
p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) )
;
hence
(
tricord1 p1,
p2,
p3,
p < 0 or
tricord2 p1,
p2,
p3,
p < 0 or
tricord3 p1,
p2,
p3,
p < 0 )
by A1, A2, Def11, Def12, Def13;
verum
end;
p in the carrier of (TOP-REAL 2)
;
then
p in REAL 2
by EUCLID:25;
then A3:
p in plane p1,p2,p3
by A1, Th63;
then consider a2, a3 being Real such that
A4:
( ((tricord1 p1,p2,p3,p) + a2) + a3 = 1 & p = (((tricord1 p1,p2,p3,p) * p1) + (a2 * p2)) + (a3 * p3) )
by A1, Def11;
assume A5:
( tricord1 p1,p2,p3,p < 0 or tricord2 p1,p2,p3,p < 0 or tricord3 p1,p2,p3,p < 0 )
; p in outside_of_triangle p1,p2,p3
( a2 = tricord2 p1,p2,p3,p & a3 = tricord3 p1,p2,p3,p )
by A1, A3, A4, Def12, Def13;
hence
p in outside_of_triangle p1,p2,p3
by A5, A4; verum