:: deftheorem defines with_implication PL_AXIOM:def 8 :
for D being Subset of PL-WFF holds
( D is with_implication iff for p, q being Element of PL-WFF st p in D & q in D holds
p => q in D );