let t, u, v be GRZ-formula; :: thesis: ( t '=' u is LD-provable implies (t '=' v) '=' (u '=' v) is LD-provable )
assume A1: t '=' u is LD-provable ; :: thesis: (t '=' v) '=' (u '=' v) is LD-provable
(t '=' u) => ((t '=' v) '=' (u '=' v)) is LD-provable ;
hence (t '=' v) '=' (u '=' v) is LD-provable by A1, Th62; :: thesis: verum