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