thus ( D is with_implication 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_implication )
assume A1: for p, q being Element of HP-WFF st p in D & q in D holds
p => q in D ; :: thesis: D is with_implication
let p, q be FinSequence; :: according to HILBERT1:def 2 :: thesis: ( not p in D or not q in D or (<*1*> ^ p) ^ q in D )
assume A2: ( p in D & q in D ) ; :: thesis: (<*1*> ^ p) ^ q in D
then reconsider p9 = p, q9 = q as Element of HP-WFF ;
p9 => q9 in D by A1, A2;
hence (<*1*> ^ p) ^ q in D ; :: thesis: verum