let A be non degenerated commutative Ring; :: thesis: ( ( for m1, m2 being object st m1 in m-Spectrum A & m2 in m-Spectrum A holds
m1 = m2 ) implies A is local )
assume A1: for m1, m2 being object st m1 in m-Spectrum A & m2 in m-Spectrum A holds
m1 = m2 ; :: thesis: A is local
reconsider m = the maximal Ideal of A as maximal Ideal of A ;
A3: for o being object st o = m holds
o in m-Spectrum A ;
m in m-Spectrum A ;
then for o being object st o in m-Spectrum A holds
o = m by A1;
then m-Spectrum A = {m} by A3, TARSKI:def 1;
hence A is local ; :: thesis: verum