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