theorem :: GRZLOG_1:26

for t, u being GRZ-formula st t '=' u is LD-provable holds
u '=' t is LD-provable by Th70, XBOOLE_1:7;