theorem Th76: :: GRZLOG_1:29

for t, u being GRZ-formula st t LD-= u holds
'not' t LD-= 'not' u