let X be non empty set ; :: thesis: 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
let F be SetSequence of X; :: thesis: ( F is non-ascending implies 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 )
assume A1: F is non-ascending ; :: thesis: 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
let S be sequence of X; :: thesis: ( ( for n being Nat holds S . n in F . n ) & rng S is finite implies not meet F is empty )
assume A2: for n being Nat holds S . n in F . n ; :: thesis: ( not rng S is finite or not meet F is empty )
A3: dom S = NAT by FUNCT_2:def 1;
assume rng S is finite ; :: thesis: not meet F is empty
then consider x being object such that
x in rng S and
A4: S " {x} is infinite by A3, CARD_2:101;

now :: thesis: for n being Nat holds x in F . n

let n be Nat; :: thesis: x in F . n
ex i being Nat st
( x in F . i & i >= n )

proof

assume A5: for i being Nat st x in F . i holds
i < n ; :: thesis: contradiction
S " {x} c= Segm n

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S " {x} or y in Segm n )
assume A6: y in S " {x} ; :: thesis: y in Segm n
reconsider i = y as Nat by A6;
S . i in {x} by A6, FUNCT_1:def 7;
then A7: S . i = x by TARSKI:def 1;
S . i in F . i by A2;
then i < n by A5, A7;
hence y in Segm n by NAT_1:44; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum

end;

then consider i being Nat such that
A8: x in F . i and
A9: i >= n ;
F . i c= F . n by A1, A9, PROB_1:def 4;
hence x in F . n by A8; :: thesis: verum

end;

hence not meet F is empty by KURATO_0:3; :: thesis: verum