( the carrier of V is Subset of V iff the carrier of V c= the carrier of V ) ;
then reconsider V1 = the carrier of V as Subset of V ;
( the addF of V = the addF of V || V1 & the lmult of V = the lmult of V | [: the carrier of R,V1:] ) by RELSET_1:19;
then ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is Submodule of V by Th40;
hence ex b₁ being Submodule of V st b₁ is strict ; :: thesis: verum