let A be non degenerated commutative Ring; :: thesis: for q being proper Ideal of A st sqrt q is maximal holds
q is primary
let q be proper Ideal of A; :: thesis: ( sqrt q is maximal implies q is primary )
set m = sqrt q;
assume A1: sqrt q is maximal ; :: thesis: q is primary
then A2: (canHom q) .: (sqrt q) is maximal by TOPZARI1:20, Th30;
reconsider M = (canHom q) .: (sqrt q) as Ideal of (A / q) by Th19;
A3: A / q is local by A1, Th38;
for x being Element of (A / q) st x is zero_divisible holds
x is nilpotent

proof

let x be Element of (A / q); :: thesis: ( x is zero_divisible implies x is nilpotent )
assume A4: x is zero_divisible ; :: thesis: x is nilpotent
x is NonUnit of (A / q)

proof

assume x is not NonUnit of (A / q) ; :: thesis: contradiction
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: verum

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: verum

end;

hence q is primary by Th35; :: thesis: verum