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