theorem Th80: :: GRZLOG_1:32

for t, u being GRZ-formula holds
( t LD-= u iff LD-EqClassOf t = LD-EqClassOf u )