theorem :: GRZLOG_1:25

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