deffunc H₁( GRZ-formula, GRZ-formula) -> GRZ-formula = $1 '=' $2;
defpred S₁[ GRZ-formula, GRZ-formula] means $1 '=' $2 is LD-provable ;
A2: for t, u, v being GRZ-formula st S₁[t,u] & S₁[u,v] holds
S₁[t,v] by Th74;
A3: for t, u being GRZ-formula holds S₁[H₁(t,u),H₁(u,t)] ;
A4: for t, u, v being GRZ-formula st S₁[t,u] holds
S₁[H₁(t,v),H₁(u,v)] by Lm78a;
for t, u, v, w being GRZ-formula st S₁[t,u] & S₁[v,w] holds
S₁[H₁(t,v),H₁(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 ; :: thesis: verum