:: deftheorem defines 'or' GRZLOG_1:def 46 :
for x, y being LD-EqClass holds x 'or' y = 'not' (('not' x) '&' ('not' y));