i in G_INT_SET ;
hence In (i,G_INT_SET) = i by SUBSET_1:def 8; :: thesis: verum