( 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 Mult of V = the Mult of V | [:INT,V1:] ) by RELSET_1:19;
then Z_ModuleStruct(# the carrier of V,(0. V), the addF of V, the Mult of V #) is Submodule of V by Th40;
hence ex b₁ being Submodule of V st b₁ is strict ; :: thesis: verum