:: deftheorem defines R-orthonormal EUCLID_7:def 5 :
for B0 being set holds
( B0 is R-orthonormal iff ( B0 is R-orthogonal & B0 is R-normal ) );