let x be object ; :: thesis: ( x in G_RAT_SET implies x is G_RAT )
assume x in G_RAT_SET ; :: thesis: x is G_RAT
then ex z being G_RAT st x = z ;
hence x is g_rational Complex ; :: thesis: verum