let X be RealUnitarySpace; :: thesis: {} is OrthogonalFamily of X
A1: {} is Subset of X by SUBSET_1:1;
for x, y being Point of X st x in {} & y in {} & x <> y holds
x .|. y = 0 ;
hence {} is OrthogonalFamily of X by A1, Def8; :: thesis: verum