let x be LD-EqClass; :: thesis: ex t, u being GRZ-formula st
( x = LD-EqClassOf t & x = LD-EqClassOf u & x = LD-EqClassOf (t '&' u) )
consider t being GRZ-formula such that
A1: x = LD-EqClassOf t by Th88;
take t ; :: thesis: ex u being GRZ-formula st
( x = LD-EqClassOf t & x = LD-EqClassOf u & x = LD-EqClassOf (t '&' u) )
take t ; :: thesis: ( x = LD-EqClassOf t & x = LD-EqClassOf t & x = LD-EqClassOf (t '&' t) )
t '=' (t '&' t) is LD-provable ;
hence ( x = LD-EqClassOf t & x = LD-EqClassOf t & x = LD-EqClassOf (t '&' t) ) by A1, Th80, Def76; :: thesis: verum