:: deftheorem defines angle EUCLID_3:def 4 :
for p1, p2, p3 being Point of (TOP-REAL 2) holds angle (p1,p2,p3) = angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3));