let p1, p2, p3 be Point of (TOP-REAL 2); ( p2 - p1,p3 - p1 are_lindependent2 implies not inside_of_triangle (p1,p2,p3) is empty )
assume A1:
p2 - p1,p3 - p1 are_lindependent2
; not inside_of_triangle (p1,p2,p3) is empty
set p0 = (((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3);
set i01 = tricord1 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3)));
set i02 = tricord2 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3)));
set i03 = tricord3 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3)));
(((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3) in the carrier of (TOP-REAL 2)
;
then
(((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3) in REAL 2
by EUCLID:22;
then A2:
( ((1 / 3) + (1 / 3)) + (1 / 3) = 1 & (((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3) in plane (p1,p2,p3) )
by A1, Th54;
then A3:
1 / 3 = tricord3 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3)))
by A1, Def13;
( 1 / 3 = tricord1 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3))) & 1 / 3 = tricord2 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3))) )
by A1, A2, Def11, Def12;
hence
not inside_of_triangle (p1,p2,p3) is empty
by A1, A3, Th58; verum