for X being RealUnitarySpace
for Y being OrthogonalFamily of X
for Z being Subset of X st Z is Subset of Y holds
Z is OrthogonalFamily of X