theorem Th46: :: EUCLID_7:47

for n being Nat
for B being Subset of (RealVectSpace (Seg n)) st B is Basis of RealVectSpace (Seg n) holds
card B = n