theorem Th8: :: KURATO_0:8

for X being set
for F being SetSequence of X holds lim_sup F c= Union F