:: deftheorem Def2 defines ** LTLAXIO3:def 2 :
for D, b₂ being set holds
( b₂ = D ** iff for x being set holds
( x in b₂ iff x is one-to-one FinSequence of D ) );