{} (REAL n) is R-orthonormal ;
hence ex b₁ being Subset of (REAL n) st b₁ is R-orthonormal ; :: thesis: verum