:: deftheorem defines semi-local TOPZARI1:def 10 :
for A being non degenerated commutative Ring holds
( A is semi-local iff m-Spectrum A is finite );