theorem Th44: :: GRZLOG_1:13

for A, A1 being non empty Subset of GRZ-formula-set
for R, R1 being GRZ-rule
for P being GRZ-formula-sequence st A c= A1 & R c= R1 & P is A,R -correct holds
P is A1,R1 -correct by Lm44;