let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p2 - p1,p3 - p1 are_lindependent2 implies not inside_of_triangle (p1,p2,p3) is empty )
assume A1: p2 - p1,p3 - p1 are_lindependent2 ; :: thesis: 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; :: thesis: verum