deffunc H1( GRZ-formula, GRZ-formula) -> GRZ-formula = $1 '=' $2;
defpred S1[ GRZ-formula, GRZ-formula] means $1 '=' $2 is LD-provable ;
A2:
for t, u, v being GRZ-formula st S1[t,u] & S1[u,v] holds
S1[t,v]
by Th74;
A3:
for t, u being GRZ-formula holds S1[H1(t,u),H1(u,t)]
;
A4:
for t, u, v being GRZ-formula st S1[t,u] holds
S1[H1(t,v),H1(u,v)]
by Lm78a;
for t, u, v, w being GRZ-formula st S1[t,u] & S1[v,w] holds
S1[H1(t,v),H1(u,w)]
from GRZLOG_1:sch 1(A2, A3, A4);
hence
for t, u, v, w being GRZ-formula st t LD-= u & v LD-= w holds
t '=' v LD-= u '=' w
; verum