theorem :: GRZLOG_1:38

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