let A be non degenerated commutative Ring; :: thesis: for J being proper Ideal of A st ( for x being object st x in ([#] A) \ J holds
x is Unit of A ) holds
A is local
let J be proper Ideal of A; :: thesis: ( ( for x being object st x in ([#] A) \ J holds
x is Unit of A ) implies A is local )
assume A1: for x being object st x in ([#] A) \ J holds
x is Unit of A ; :: thesis: A is local
consider m1 being maximal Ideal of A such that
A2: J c= m1 by Th10;
A3: for m being maximal Ideal of A holds m = m1

proof

let m be maximal Ideal of A; :: thesis: m = m1
for o being object st o in m holds
o in m1

proof

let o be object ; :: thesis: ( o in m implies o in m1 )
assume A4: o in m ; :: thesis: o in m1
then o is NonUnit of A by Th15;
then not o in ([#] A) \ J by A1;
then o in J by A4, XBOOLE_0:def 5;
hence o in m1 by A2; :: thesis: verum

end;

then m c= m1 ;
hence m = m1 by RING_1:def 3; :: thesis: verum

end;

for o1, o2 being object st o1 in m-Spectrum A & o2 in m-Spectrum A holds
o1 = o2

proof

let o1, o2 be object ; :: thesis: ( o1 in m-Spectrum A & o2 in m-Spectrum A implies o1 = o2 )
assume that
A8: o1 in m-Spectrum A and
A9: o2 in m-Spectrum A ; :: thesis: o1 = o2
consider x1 being maximal Ideal of A such that
A10: x1 = o1 by A8;
consider x2 being maximal Ideal of A such that
A11: x2 = o2 by A9;
o1 = m1 by A10, A3
.= o2 by A3, A11 ;
hence o1 = o2 ; :: thesis: verum

end;

hence A is local by Th16; :: thesis: verum