theorem Th79: :: SETLIM_1:79

for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V56() holds
lim_inf S = Union S by Th46;