let A be non degenerated commutative Ring; :: thesis: for S being non empty Subset of A holds Ideals (A,S) = Ideals (A,(S -Ideal))
let S be non empty Subset of A; :: thesis: Ideals (A,S) = Ideals (A,(S -Ideal))
thus Ideals (A,S) c= Ideals (A,(S -Ideal)) :: according to XBOOLE_0:def 10 :: thesis: Ideals (A,(S -Ideal)) c= Ideals (A,S)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ideals (A,S) or x in Ideals (A,(S -Ideal)) )
assume x in Ideals (A,S) ; :: thesis: x in Ideals (A,(S -Ideal))
then consider y being Ideal of A such that
A2: x = y and
A3: S c= y ;
S -Ideal c= y -Ideal by A3, IDEAL_1:57;
then S -Ideal c= y by IDEAL_1:44;
hence x in Ideals (A,(S -Ideal)) by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ideals (A,(S -Ideal)) or x in Ideals (A,S) )
assume x in Ideals (A,(S -Ideal)) ; :: thesis: x in Ideals (A,S)
then consider y being Ideal of A such that
A8: x = y and
A9: S -Ideal c= y ;
S c= S -Ideal by IDEAL_1:def 14;
then S c= y by A9;
hence x in Ideals (A,S) by A8; :: thesis: verum