:: deftheorem defines orthogonal_basis EUCLID_7:def 7 :
for n being Nat
for B0 being Subset of (REAL n) holds
( B0 is orthogonal_basis iff ( B0 is R-orthonormal & B0 is complete ) );