now :: thesis: for x being object st x in { z where z is G_RAT : verum } holds
x in COMPLEX

let x be object ; :: thesis: ( x in { z where z is G_RAT : verum } implies x in COMPLEX )
assume x in { z where z is G_RAT : verum } ; :: thesis: x in COMPLEX
then ex z being G_RAT st x = z ;
hence x in COMPLEX by XCMPLX_0:def 2; :: thesis: verum

end;

hence { z where z is G_RAT : verum } is Subset of COMPLEX by TARSKI:def 3; :: thesis: verum