set A = the Subspace of VS;
for X being set st X in { the Subspace of VS} holds
X is Subspace of VS by TARSKI:def 1;
then reconsider B = { the Subspace of VS} as SubVS-Family of VS by Def2;
take B ; :: thesis: not B is empty
thus not B is empty ; :: thesis: verum