let x be object ; :: thesis: ( x in G_INT_SET implies x is G_INTEG )
assume x in G_INT_SET ; :: thesis: x is G_INTEG
then ex z being G_INTEG st x = z ;
hence x is g_integer Complex ; :: thesis: verum