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:25;
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, Th63;
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, Th67; :: thesis: verum