theorem :: GRZLOG_1:19

for A, A1 being non empty Subset of GRZ-formula-set
for R, R1 being GRZ-rule
for t being GRZ-formula st A c= A1 & R c= R1 & A,R |- t holds
A1,R1 |- t by Th44;