:: deftheorem defines Euclidean EUCLMETR:def 1 :
for IT being OrtAfSp holds
( IT is Euclidean iff for a, b, c, d being Element of IT st a,b _|_ c,d & b,c _|_ a,d holds
b,d _|_ a,c );