theorem Th7: :: RLVECT_3:7

for V being RealLinearSpace holds {} the carrier of V is linearly-independent