let A be non degenerated commutative Ring; :: thesis: ex E being non empty Subset of A st Spectrum A = PrimeIdeals (A,E)
take {(0. A)} ; :: thesis: Spectrum A = PrimeIdeals (A,{(0. A)})
thus Spectrum A = PrimeIdeals (A,{(0. A)}) by Th21; :: thesis: verum