:: deftheorem defines |{ EUCLID_5:def 5 :
for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |(p1,(p2 <X> p3))|;