for F being Subset of PL-WFF
for A being Element of PL-WFF holds
( F |- A iff ex G being Subset of PL-WFF st
( G c= F & G is finite & G |- A ) )