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