let x be LD-EqClass; :: thesis: ex t being GRZ-formula st x = LD-EqClassOf t
x in Class LD-EqR ;
then consider a being object such that
A1: a in GRZ-formula-set and
A2: x = Class (LD-EqR,a) by EQREL_1:def 3;
reconsider t = a as GRZ-formula by A1;
take t ; :: thesis: x = LD-EqClassOf t
thus x = LD-EqClassOf t by A2; :: thesis: verum