0. A is Zero_Divisor of A by Th1;
then 0. A in ZeroDiv_Set A ;
then not 0. A in Non_ZeroDiv_Set A by XBOOLE_0:def 5;
hence not Total-Quotient-Ring A is degenerated by Th31; :: thesis: verum