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