theorem :: BHSP_1:23

for X being RealUnitarySpace
for x being Point of X holds x, 0. X are_orthogonal by Th14;