theorem :: KURATO_0:21

for T being set
for F being SetSequence of T st F is non-descending holds
lim_sup F = Union F