set a = 1. A;
not 1. A in ZeroDiv_Set A
proof
assume 1. A in ZeroDiv_Set A ; :: thesis: contradiction
then ex a1 being Element of [#] A st
( a1 = 1. A & a1 is Zero_Divisor of A ) ;
hence contradiction by Th2; :: thesis: verum
end;
hence not Non_ZeroDiv_Set A is empty by XBOOLE_0:def 5; :: thesis: verum