:: deftheorem defines 'not' GRZLOG_1:def 11 :
for t being GRZ-formula holds 'not' t = (Polish-unOp (GRZ-symbols,GRZ-arity,'not')) . t;