theorem :: GRZLOG_1:39

for t, u being GRZ-formula holds LD-EqClassOf (t '=' u) = (LD-EqClassOf t) '=' (LD-EqClassOf u) by Def93;