reconsider W = [#] V as non empty Subset of V ;

A1: W is Cadditively-linearly-closed ;

W is multiplicatively-closed ;

hence ex b_{1} being non empty Subset of V st

( b_{1} is Cadditively-linearly-closed & b_{1} is multiplicatively-closed )
by A1; :: thesis: verum

A1: W is Cadditively-linearly-closed ;

W is multiplicatively-closed ;

hence ex b

( b