assume not NonZero S is empty ; :: thesis: contradiction
then consider x being Element of S such that
W1: x in NonZero S by SUBSET_1:4;
not x in {(0. S)} by W1, XBOOLE_0:def 5;
then x <> 0. S by TARSKI:def 1;
hence contradiction by Def19; :: thesis: verum