:: deftheorem defines GRZ-formula-set GRZLOG_1:def 9 :
GRZ-formula-set = Polish-WFF-set (GRZ-symbols,GRZ-arity);