reconsider W = [#] V as non empty Subset of V ;
A1: W is Cadditively-linearly-closed ;
W is multiplicatively-closed ;
hence ex b₁ being non empty Subset of V st
( b₁ is Cadditively-linearly-closed & b₁ is multiplicatively-closed ) by A1; :: thesis: verum