let t, u, v be GRZ-formula; :: thesis: ( t '=' u is LD-provable & u '=' v is LD-provable implies t '=' v is LD-provable )
assume that
A1: t '=' u is LD-provable and
A2: u '=' v is LD-provable ; :: thesis: t '=' v is LD-provable
A3: u '=' t is LD-provable by A1, Th70, XBOOLE_1:7;
set w = (u '=' v) '=' (t '=' v);
(u '=' t) => ((u '=' v) '=' (t '=' v)) is LD-provable ;
then (u '=' v) '=' (t '=' v) is LD-provable by A3, Th62;
hence t '=' v is LD-provable by A2, Th61; :: thesis: verum