let V be non empty RLSStruct ; :: thesis: for M being Subset of V st M = {} holds
M is cone
let M be Subset of V; :: thesis: ( M = {} implies M is cone )
A1: for r being Real
for v being VECTOR of V st r > 0 & v in {} holds
r * v in {} ;
assume M = {} ; :: thesis: M is cone
hence M is cone by A1, Def3; :: thesis: verum