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