set M = {(0. V)};
reconsider M = {(0. V)} as Subset of V ;
for r being Real
for v being VECTOR of V st r > 0 & v in M holds
r * v in M

proof

let r be Real; :: thesis: for v being VECTOR of V st r > 0 & v in M holds
r * v in M
let v be VECTOR of V; :: thesis: ( r > 0 & v in M implies r * v in M )
assume that
r > 0 and
A1: v in M ; :: thesis: r * v in M
v = 0. V by A1, TARSKI:def 1;
then r * v = 0. V ;
hence r * v in M by TARSKI:def 1; :: thesis: verum

end;

then reconsider M = M as cone Subset of V by Def3;
take M ; :: thesis: ( not M is empty & M is cone )
thus ( not M is empty & M is cone ) ; :: thesis: verum