theorem Th88: :: GRZLOG_1:33

for x being LD-EqClass ex t being GRZ-formula st x = LD-EqClassOf t