let A be non degenerated commutative Ring; :: thesis: for S being non empty Subset of A holds PrimeIdeals (A,S) = PrimeIdeals (A,(S -Ideal))
let S be non empty Subset of A; :: thesis: PrimeIdeals (A,S) = PrimeIdeals (A,(S -Ideal))
PrimeIdeals (A,S) = (Ideals (A,S)) /\ (Spectrum A) by Th33
.= (Ideals (A,(S -Ideal))) /\ (Spectrum A) by Th2
.= PrimeIdeals (A,(S -Ideal)) by Th33 ;
hence PrimeIdeals (A,S) = PrimeIdeals (A,(S -Ideal)) ; :: thesis: verum