consider t being GRZ-formula such that
A1: x = LD-EqClassOf t by Th88;
consider u being GRZ-formula such that
A2: y = LD-EqClassOf u by Th88;
take LD-EqClassOf (t '=' u) ; :: thesis: ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & LD-EqClassOf (t '=' u) = LD-EqClassOf (t '=' u) )
thus ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & LD-EqClassOf (t '=' u) = LD-EqClassOf (t '=' u) ) by A1, A2; :: thesis: verum