set M = the carrier of V;
for u being set st u in the carrier of V holds
u in the carrier of V ;
then reconsider M = the carrier of V as Subset of V by TARSKI:def 3;
reconsider M = M as non empty Subset of V ;
take M ; :: thesis: ( M is add-closed & M is multi-closed & not M is empty )
( ( for a being Real
for v being VECTOR of V st v in M holds
a * v in M ) & ( for x, y being Element of V st x in M & y in M holds
x + y in M ) ) ;
hence ( M is add-closed & M is multi-closed & not M is empty ) by Def1, IDEAL_1:def 1; :: thesis: verum