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
assume A2:
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 )
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;
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 )
; 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; verum