:: deftheorem defines LD-EqClassOf GRZLOG_1:def 41 :
for t being GRZ-formula holds LD-EqClassOf t = Class (LD-EqR,t);