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