theorem Th24: :: COMPL_SP:25

for X being non empty set
for F being SetSequence of X st F is non-ascending holds
for S being sequence of X st ( for n being Nat holds S . n in F . n ) & rng S is finite holds
not meet F is empty