set C = { I where I is Ideal of R : verum } ;

now :: thesis: for x being object st x in { I where I is Ideal of R : verum } holds
x in bool the carrier of R

let x be object ; :: thesis: ( x in { I where I is Ideal of R : verum } implies x in bool the carrier of R )
assume x in { I where I is Ideal of R : verum } ; :: thesis: x in bool the carrier of R
then ex I being Ideal of R st x = I ;
hence x in bool the carrier of R ; :: thesis: verum

end;

then { I where I is Ideal of R : verum } c= bool the carrier of R ;
hence { I where I is Ideal of R : verum } is Subset-Family of the carrier of R ; :: thesis: verum