theorem Th20: :: HAHNBAN1:22

for V being VectSp of F_Complex
for M being Subspace of V holds RealVS M is Subspace of RealVS V