let t be GRZ-formula; :: thesis: t '=' t is LD-provable
set u = t '&' t;
A2: t '=' (t '&' t) is LD-provable ;
then (t '&' t) '=' t is LD-provable by Th70, XBOOLE_1:7;
hence t '=' t is LD-provable by A2, Th74; :: thesis: verum