thus ( D is with_conjunction implies for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D ) ; :: thesis: ( ( for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D ) implies D is with_conjunction )
assume A3: for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D ; :: thesis: D is with_conjunction
let p, q be FinSequence; :: according to HILBERT1:def 3 :: thesis: ( not p in D or not q in D or (<*2*> ^ p) ^ q in D )
assume A4: ( p in D & q in D ) ; :: thesis: (<*2*> ^ p) ^ q in D
then reconsider p9 = p, q9 = q as Element of HP-WFF ;
p9 '&' q9 in D by A3, A4;
hence (<*2*> ^ p) ^ q in D ; :: thesis: verum