theorem Th82: :: SETLIM_1:82

for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is V55() holds
lim_inf S = Intersection S by Th53;