:: deftheorem defines inside_of_triangle EUCLID_3:def 7 :
for n being Element of NAT
for p1, p2, p3 being Point of (TOP-REAL n) holds inside_of_triangle (p1,p2,p3) = (closed_inside_of_triangle (p1,p2,p3)) \ (Triangle (p1,p2,p3));