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

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