theorem Th78: :: GRZLOG_1:31

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