:: deftheorem Def2 defines with_implication HILBERT1:def 2 :
for D being set holds
( D is with_implication iff for p, q being FinSequence st p in D & q in D holds
(<*1*> ^ p) ^ q in D );