theorem :: EUCLID_7:52

for n being Nat
for B being Orthogonal_Basis of n holds card B = n