let S be ZeroStr ; :: thesis: not 0. S in NonZero S
assume 0. S in NonZero S ; :: thesis: contradiction
then not 0. S in {(0. S)} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum