theorem th37: :: PL_AXIOM:68

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