theorem Th62: :: GRZLOG_1:22

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