let z1, z2 be LD-EqClass; :: thesis: ( ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & z1 = LD-EqClassOf (t '=' u) ) & ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & z2 = LD-EqClassOf (t '=' u) ) implies z1 = z2 )
given t1, u1 being GRZ-formula such that A1: x = LD-EqClassOf t1 and
A2: y = LD-EqClassOf u1 and
A3: z1 = LD-EqClassOf (t1 '=' u1) ; :: thesis: ( for t, u being GRZ-formula holds
( not x = LD-EqClassOf t or not y = LD-EqClassOf u or not z2 = LD-EqClassOf (t '=' u) ) or z1 = z2 )
given t2, u2 being GRZ-formula such that A4: x = LD-EqClassOf t2 and
A5: y = LD-EqClassOf u2 and
A6: z2 = LD-EqClassOf (t2 '=' u2) ; :: thesis: z1 = z2
A7: t1 LD-= t2 by A1, A4, Th80;
u1 LD-= u2 by A2, A5, Th80;
hence z1 = z2 by A3, A6, A7, Th78, Th80; :: thesis: verum