theorem :: GRZLOG_1:18

for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for t being GRZ-formula holds
( not A,R |- t or t in A or ex S being GRZ-formula-finset st
( [S,t] in R & A,R |- S ) )