theorem Th42: :: GRZLOG_1:11

for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for P1, P2 being GRZ-formula-sequence st P1 is A,R -correct & P2 is A,R -correct holds
P1 ^ P2 is A,R -correct