theorem :: SETLIM_1:27

for n being Nat
for X being set
for B being SetSequence of X holds (superior_setsequence B) . n c= Union B