:: deftheorem defines G_INT_SET GAUSSINT:def 2 :
G_INT_SET = { z where z is G_INTEG : verum } ;