:: deftheorem Def6 defines with_modal_operator INTPRO_1:def 6 :
for E being set holds
( E is with_modal_operator iff for p being FinSequence st p in E holds
<*6*> ^ p in E );