theorem :: BHSP_1:1

for X being RealUnitarySpace holds (0. X) .|. (0. X) = 0 by Def2;