theorem Th26: :: RLSUB_1:26
for V, X being strict RealLinearSpace st V is Subspace of X & X is Subspace of V holds
V = X