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