:: deftheorem Def91 defines 'not' GRZLOG_1:def 43 :
for x, b₂ being LD-EqClass holds
( b₂ = 'not' x iff ex t being GRZ-formula st
( x = LD-EqClassOf t & b₂ = LD-EqClassOf ('not' t) ) );