theorem Th7: :: KURATO_0:7

for X being set
for F being SetSequence of X holds meet F c= lim_inf F