theorem Th5: :: BHSP_7:5

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