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

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