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