theorem conco: :: PL_AXIOM:62

for F being Subset of PL-WFF holds
( F is consistent iff not for A being Element of PL-WFF holds F |- A )