:: deftheorem defines are_orthogonal BHSP_1:def 3 :
for X being RealUnitarySpace
for x, y being Point of X holds
( x,y are_orthogonal iff x .|. y = 0 );