assume x is not NonUnit of (A / q) ; :: thesis:
then x in { a where a is Element of (A / q) : a is Unit of (A / q) } ;
then x in Unit_Set (A / q) by RINGFRAC:def 5;
then consider a1 being Element of (A / q) such that
A6: x * a1 = 1. (A / q) by Lm3;
consider y being Element of (A / q) such that
A7: ( y <> 0. (A / q) & y * x = 0. (A / q) ) by A4;
y = y * (1. (A / q))
.= (y * x) * a1 by A6, GROUP_1:def 3
.= 0. (A / q) by A7 ;
hence contradiction by A7; :: thesis:

end;

then consider m1 being maximal Ideal of (A / q) such that
A8: x in m1 by TOPZARI1:10;
set S = { I where I is Ideal of (A / q) : ( I is quasi-maximal & I <> [#] (A / q) ) } ;
M in { I where I is Ideal of (A / q) : ( I is quasi-maximal & I <> [#] (A / q) ) } by A2;
then A9: M in m-Spectrum (A / q) by TOPZARI1:def 7;
m1 in { I where I is Ideal of (A / q) : ( I is quasi-maximal & I <> [#] (A / q) ) } ;
then A10: m1 in m-Spectrum (A / q) by TOPZARI1:def 7;
consider M0 being Ideal of (A / q) such that
A11: m-Spectrum (A / q) = {M0} by A3;
M = M0 by A9, A11, TARSKI:def 1
.= m1 by A10, A11, TARSKI:def 1 ;
then x in nilrad (A / q) by Th37, A8;
then x in { a where a is nilpotent Element of (A / q) : verum } by TOPZARI1:def 13;
then consider x0 being nilpotent Element of (A / q) such that
A13: x0 = x ;
thus x is nilpotent by A13; :: thesis:

end;