:: deftheorem Def9 defines inferior_setsequence BOR_CANT:def 9 :
for X being set
for A, b₃ being SetSequence of X holds
( b₃ = inferior_setsequence A iff for n being Nat holds b₃ . n = Intersection (A ^\ n) );