let T be set ; :: thesis: for F being SetSequence of T
for x being object st F is non-ascending & ex k being Nat st
for n being Nat st n > k holds
x in F . n holds
x in meet F
let F be SetSequence of T; :: thesis: for x being object st F is non-ascending & ex k being Nat st
for n being Nat st n > k holds
x in F . n holds
x in meet F
let x be object ; :: thesis: ( F is non-ascending & ex k being Nat st
for n being Nat st n > k holds
x in F . n implies x in meet F )
assume A1: F is non-ascending ; :: thesis: ( for k being Nat ex n being Nat st
( n > k & not x in F . n ) or x in meet F )
given k being Nat such that A2: for n being Nat st n > k holds
x in F . n ; :: thesis: x in meet F
k + 1 > k by NAT_1:13;
then A3: x in F . (k + 1) by A2;
assume not x in meet F ; :: thesis: contradiction
then not x in meet (rng F) by FUNCT_6:def 4;
then consider Y being set such that
A4: Y in rng F and
A5: not x in Y by SETFAM_1:def 1;
consider y being object such that
A6: y in dom F and
A7: Y = F . y by A4, FUNCT_1:def 3;
reconsider y = y as Nat by A6;

per cases ( y > k or y <= k ) ;

suppose y > k ; :: thesis: contradiction

hence contradiction by A2, A5, A7; :: thesis: verum

end;

suppose y <= k ; :: thesis: contradiction

then F . k c= F . y by A1, PROB_1:def 4;
then A8: not x in F . k by A5, A7;
F . (k + 1) c= F . k by A1;
hence contradiction by A3, A8; :: thesis: verum

end;

end;