theorem Th28: :: SETLIM_1:28

for X being set
for B being SetSequence of X
for n being Nat holds { (B . k) where k is Nat : n <= k } is Subset-Family of X