:: deftheorem Def2 defines ||^ IDEAL_2:def 2 :
for K being non empty doubleLoopStr
for S being Subset of K
for n being Nat
for b₄ being Subset of K holds
( ( n = 0 implies ( b₄ = S ||^ n iff b₄ = the carrier of K ) ) & ( not n = 0 implies ( b₄ = S ||^ n iff ex f being FinSequence of bool the carrier of K st
( b₄ = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) ) ) ) ) );