theorem :: CSSPACE:37

for X being ComplexUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
- x,y are_orthogonal