theorem :: GRZLOG_1:37

for t being GRZ-formula holds LD-EqClassOf ('not' t) = 'not' (LD-EqClassOf t) by Def91;