theorem :: GRZLOG_1:10

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