set C = { I where I is Ideal of A : S c= I } ;
now :: thesis: for x being object st x in { I where I is Ideal of A : S c= I } holds
x in Ideals A
let x be object ; :: thesis: ( x in { I where I is Ideal of A : S c= I } implies x in Ideals A )
assume x in { I where I is Ideal of A : S c= I } ; :: thesis: x in Ideals A
then ex I being Ideal of A st
( x = I & S c= I ) ;
hence x in Ideals A by Lm1; :: thesis: verum
end;
then { I where I is Ideal of A : S c= I } c= Ideals A ;
hence { I where I is Ideal of A : S c= I } is Subset of (Ideals A) ; :: thesis: verum