let A be non degenerated commutative Ring; :: thesis: for S being non empty Subset of A holds PrimeIdeals (A,S) = (Ideals (A,S)) /\ (Spectrum A)
let S be non empty Subset of A; :: thesis: PrimeIdeals (A,S) = (Ideals (A,S)) /\ (Spectrum A)
thus PrimeIdeals (A,S) c= (Ideals (A,S)) /\ (Spectrum A) :: according to XBOOLE_0:def 10 :: thesis: (Ideals (A,S)) /\ (Spectrum A) c= PrimeIdeals (A,S)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeIdeals (A,S) or x in (Ideals (A,S)) /\ (Spectrum A) )
assume A2: x in PrimeIdeals (A,S) ; :: thesis: x in (Ideals (A,S)) /\ (Spectrum A)
then consider x1 being prime Ideal of A such that
A3: x1 = x and
S c= x1 ;
A4: x in Spectrum A by A3;
x in Ideals (A,S) by A2, Th32, TARSKI:def 3;
hence x in (Ideals (A,S)) /\ (Spectrum A) by A4, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Ideals (A,S)) /\ (Spectrum A) or x in PrimeIdeals (A,S) )
assume x in (Ideals (A,S)) /\ (Spectrum A) ; :: thesis: x in PrimeIdeals (A,S)
then A8: ( x in Ideals (A,S) & x in Spectrum A ) by XBOOLE_0:def 4;
then consider x1 being Ideal of A such that
A10: x1 = x and
A11: S c= x1 ;
x1 is prime Ideal of A by A8, Th22, A10;
hence x in PrimeIdeals (A,S) by A10, A11; :: thesis: verum