theorem Th6: :: RLVECT_3:6

for V being RealLinearSpace
for A being Subset of V st A is linearly-independent holds
not 0. V in A