let A be non degenerated commutative Ring; :: thesis: PrimeIdeals (A,{(0. A)}) = Spectrum A
Spectrum A c= PrimeIdeals (A,{(0. A)})
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Spectrum A or x in PrimeIdeals (A,{(0. A)}) )
assume x in Spectrum A ; :: thesis: x in PrimeIdeals (A,{(0. A)})
then consider J being prime Ideal of A such that
A3: J = x ;
{(0. A)} c= J by IDEAL_1:2, ZFMISC_1:31;
hence x in PrimeIdeals (A,{(0. A)}) by A3; :: thesis: verum
end;
hence PrimeIdeals (A,{(0. A)}) = Spectrum A ; :: thesis: verum