let A be domRing; :: thesis: for a being Element of A holds
( a in Non_ZeroDiv_Set A iff a <> 0. A )
let a be Element of A; :: thesis: ( a in Non_ZeroDiv_Set A iff a <> 0. A )
thus ( a in Non_ZeroDiv_Set A implies a <> 0. A ) :: thesis: ( a <> 0. A implies a in Non_ZeroDiv_Set A )

proof

assume a in Non_ZeroDiv_Set A ; :: thesis: a <> 0. A
then a in ([#] A) \ {(0. A)} by Lm63;
then ( a in [#] A & not a in {(0. A)} ) by XBOOLE_0:def 5;
hence a <> 0. A by TARSKI:def 1; :: thesis: verum

end;

assume a <> 0. A ; :: thesis: a in Non_ZeroDiv_Set A
then not a in {(0. A)} by TARSKI:def 1;
then a in ([#] A) \ {(0. A)} by XBOOLE_0:def 5;
hence a in Non_ZeroDiv_Set A by Lm63; :: thesis: verum