theorem Th70: :: GRZLOG_1:24

for A being non empty Subset of GRZ-formula-set
for t, u being GRZ-formula st GRZ-axioms c= A & A, GRZ-rules |- t '=' u holds
A, GRZ-rules |- u '=' t