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