:: deftheorem defines Euclidean_like DIRORT:def 7 :
for IT being Oriented_Orthogonality_Space holds
( IT is Euclidean_like iff for u, u1, v, v1 being Element of IT st u,u1 '//' v,v1 holds
v,v1 '//' u1,u );