:: deftheorem defines 'or' GRZLOG_1:def 14 :
for t, u being GRZ-formula holds t 'or' u = 'not' (('not' t) '&' ('not' u));