:: deftheorem defines G_RAT_SET GAUSSINT:def 11 :
G_RAT_SET = { z where z is G_RAT : verum } ;