:: deftheorem withplax defines with_PL_axioms PL_AXIOM:def 19 :
for D being set holds
( D is with_PL_axioms iff for p, q, r being Element of PL-WFF holds
( p => (q => p) in D & (p => (q => r)) => ((p => q) => (p => r)) in D & (('not' q) => ('not' p)) => ((('not' q) => p) => q) in D ) );