let A be non degenerated commutative Ring; :: thesis: for S being non empty Subset of A holds PrimeIdeals (A,S) c= Ideals (A,S)
let S be non empty Subset of A; :: thesis: PrimeIdeals (A,S) c= Ideals (A,S)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeIdeals (A,S) or x in Ideals (A,S) )
assume x in PrimeIdeals (A,S) ; :: thesis: x in Ideals (A,S)
then consider x1 being prime Ideal of A such that
A2: x1 = x and
A3: S c= x1 ;
thus x in Ideals (A,S) by A2, A3; :: thesis: verum