theorem Th50: :: REAL_NS2:50

for n being Nat
for X being set holds
( X is Basis of (n -VectSp_over F_Real) iff X is Basis of TOP-REAL n )