:: deftheorem defines consistent PL_AXIOM:def 27 :
for F being Subset of PL-WFF holds
( F is consistent iff for p being Element of PL-WFF holds
( not F |- p or not F |- 'not' p ) );