let X be RealUnitarySpace; :: thesis: for x being Point of X holds x, 0. X are_orthogonal
let x be Point of X; :: thesis: x, 0. X are_orthogonal
x .|. H₁(X) = 0 by Th19;
hence x, 0. X are_orthogonal by Def3; :: thesis: verum