theorem Th77: :: GRZLOG_1:30

for t, u, v, w being GRZ-formula st t LD-= u & v LD-= w holds
t '&' v LD-= u '&' w