let p1, p2, p3, p be Point of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: ( 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 ) :: thesis: ( ( 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

assume A2: p in outside_of_triangle (p1,p2,p3) ; :: thesis: ( tricord1 (p1,p2,p3,p) < 0 or tricord2 (p1,p2,p3,p) < 0 or tricord3 (p1,p2,p3,p) < 0 )
p in the carrier of (TOP-REAL 2) ;
then p in REAL 2 by EUCLID:22;
then A3: p in plane (p1,p2,p3) by A1, Th54;
consider p0 being Point of (TOP-REAL 2) such that
A4: p0 = p and
A5: 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) ) by A2;
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) ) by A5;
hence ( tricord1 (p1,p2,p3,p) < 0 or tricord2 (p1,p2,p3,p) < 0 or tricord3 (p1,p2,p3,p) < 0 ) by A1, A3, Def11, Def12, Def13, A4; :: thesis: verum

end;

p in the carrier of (TOP-REAL 2) ;
then p in REAL 2 by EUCLID:22;
then A6: p in plane (p1,p2,p3) by A1, Th54;
then consider a2, a3 being Real such that
A7: ( ((tricord1 (p1,p2,p3,p)) + a2) + a3 = 1 & p = (((tricord1 (p1,p2,p3,p)) * p1) + (a2 * p2)) + (a3 * p3) ) by A1, Def11;
assume A8: ( tricord1 (p1,p2,p3,p) < 0 or tricord2 (p1,p2,p3,p) < 0 or tricord3 (p1,p2,p3,p) < 0 ) ; :: thesis: p in outside_of_triangle (p1,p2,p3)
( a2 = tricord2 (p1,p2,p3,p) & a3 = tricord3 (p1,p2,p3,p) ) by A1, A6, A7, Def12, Def13;
hence p in outside_of_triangle (p1,p2,p3) by A8, A7; :: thesis: verum