theorem :: KURATO_0:21

for T being set
for F being SetSequence of T st F is V53() holds
lim_sup F = Union F