take {} ; :: thesis: for x being set st x in {} holds
x is Subspace of VS
thus for x being set st x in {} holds
x is Subspace of VS ; :: thesis: verum