theorem Th2: :: BHSP_5:2

for X being RealUnitarySpace holds {} is OrthogonalFamily of X