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