let A be non degenerated commutative Ring; :: thesis: not 0. A in Non_ZeroDiv_Set A
0. A is Zero_Divisor of A by Th1;
then 0. A in ZeroDiv_Set A ;
hence not 0. A in Non_ZeroDiv_Set A by XBOOLE_0:def 5; :: thesis: verum