:: deftheorem defines Spectrum TOPZARI1:def 6 :
for A being non degenerated commutative Ring holds Spectrum A = { I where I is prime Ideal of A : verum } ;