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