:: deftheorem defines Spectrum LATTICEA:def 10 :
for L being Lattice holds Spectrum L = { I where I is Ideal of L : ( I is prime & I is proper ) } ;