set a = 0. A;
0. A is Zero_Divisor of A by Th1;
then 0. A in ZeroDiv_Set A ;
hence not ZeroDiv_Set A is empty ; :: thesis: verum