theorem Th43: :: GRZLOG_1:12

for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for S1, S2 being GRZ-formula-finset st S1 is A,R -correct & S2 is A,R -correct holds
S1 \/ S2 is A,R -correct