:: deftheorem Def8 defines OrthogonalFamily BHSP_5:def 8 :
for X being RealUnitarySpace
for b₂ being Subset of X holds
( b₂ is OrthogonalFamily of X iff for x, y being Point of X st x in b₂ & y in b₂ & x <> y holds
x .|. y = 0 );