theorem Th51: :: PROOFS_1:12

for B being set
for R being Rule
for a being object holds
( not B,R |- a or a in B or ex S being Formula-finset st
( [S,a] in R & ( for b being object st b in S holds
B,R |- b ) ) )