set M = { I where I is primary Ideal of A : verum } ;

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

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

end;

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