theorem finin: :: PL_AXIOM:65

for F being Subset of PL-WFF st not F is consistent holds
ex G being Subset of PL-WFF st
( G is finite & not G is consistent & G c= F )