:: deftheorem defines closed_inside_of_triangle EUCLID_3:def 6 :
for n being Element of NAT
for p1, p2, p3 being Point of (TOP-REAL n) holds closed_inside_of_triangle (p1,p2,p3) = { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ;