theorem Th80: :: REAL_NS2:80

for W being RealLinearSpace
for X being set holds
( X is Basis of (RLSp2RVSp W) iff X is Basis of W )