let A be non degenerated commutative Ring; :: thesis: for p being Element of Spectrum A holds
( A ~ p is local & Loc-Ideal p is maximal Ideal of (A ~ p) )
let p be Element of Spectrum A; :: thesis: ( A ~ p is local & Loc-Ideal p is maximal Ideal of (A ~ p) )
reconsider J = Loc-Ideal p as proper Ideal of (A ~ p) by Th53;
A1: A ~ p is local

proof

( ( for x being object st x in ([#] (A ~ p)) \ J holds
x is Unit of (A ~ p) ) implies A ~ p is local ) by TOPZARI1:13;
hence A ~ p is local by Th54; :: thesis: verum

end;

J is maximal Ideal of (A ~ p)

proof

consider m being maximal Ideal of (A ~ p) such that
A3: J c= m by TOPZARI1:8;
for o being object st o in m holds
o in J

proof

let o be object ; :: thesis: ( o in m implies o in J )
assume A4: o in m ; :: thesis: o in J
then A5: o is NonUnit of (A ~ p) by TOPZARI1:11;

per cases ( o in m \ J or not o in m \ J ) ;

suppose o in m \ J ; :: thesis: o in J

then A7: ( o in m & not o in J ) by XBOOLE_0:def 5;
o in ([#] (A ~ p)) \ J by A7, XBOOLE_0:def 5;
hence o in J by A5, Th54; :: thesis: verum

end;

suppose not o in m \ J ; :: thesis: o in J

hence o in J by A4, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

then m c= J ;
hence J is maximal Ideal of (A ~ p) by A3, XBOOLE_0:def 10; :: thesis: verum

end;

hence ( A ~ p is local & Loc-Ideal p is maximal Ideal of (A ~ p) ) by A1; :: thesis: verum