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