:: deftheorem defines local TOPZARI1:def 9 :
for A being non degenerated commutative Ring holds
( A is local iff ex m being Ideal of A st m-Spectrum A = {m} );