set M = { a where a is Element of R : 0. R <=_ Q,a } ;
{ a where a is Element of R : 0. R <=_ Q,a } c= the carrier of R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of R : 0. R <=_ Q,a } or x in the carrier of R )
assume x in { a where a is Element of R : 0. R <=_ Q,a } ; :: thesis: x in the carrier of R
then consider a being Element of R such that
A1: ( x = a & 0. R <=_ Q,a ) ;
thus x in the carrier of R by A1; :: thesis: verum

end;

hence { a where a is Element of R : 0. R <=_ Q,a } is Subset of R ; :: thesis: verum