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