theorem Th8: :: EUCLID_7:9

for V being RealLinearSpace
for X being Subspace of V st V is strict & X is strict & the carrier of X = the carrier of V holds
X = V