:: deftheorem Def6 defines complete EUCLID_7:def 6 :
for n being Nat
for B0 being Subset of (REAL n) holds
( B0 is complete iff for B being R-orthonormal Subset of (REAL n) st B0 c= B holds
B = B0 );