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