set M = { a where a is Element of R : a is square } ;

now :: thesis: for x being object st x in { a where a is Element of R : a is square } holds
x in the carrier of R

let x be object ; :: thesis: ( x in { a where a is Element of R : a is square } implies x in the carrier of R )
assume x in { a where a is Element of R : a is square } ; :: thesis: x in the carrier of R
then consider a being Element of R such that
A1: ( x = a & a is square ) ;
thus x in the carrier of R by A1; :: thesis: verum

end;

then { a where a is Element of R : a is square } c= the carrier of R ;
hence { a where a is Element of R : a is square } is Subset of R ; :: thesis: verum