let T be set ; :: thesis: for F being SetSequence of T st F is non-ascending holds
lim_inf F = meet F
let F be SetSequence of T; :: thesis: ( F is non-ascending implies lim_inf F = meet F )
assume A1: F is non-ascending ; :: thesis: lim_inf F = meet F
thus lim_inf F c= meet F :: according to XBOOLE_0:def 10 :: thesis: meet F c= lim_inf F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_inf F or x in meet F )
assume x in lim_inf F ; :: thesis: x in meet F
then consider n being Nat such that
A2: for k being Nat holds x in F . (n + k) by Th4;
for k being Nat st k > n holds
x in F . k

proof

let k be Nat; :: thesis: ( k > n implies x in F . k )
assume k > n ; :: thesis: x in F . k
then consider h being Nat such that
A3: k = n + h by NAT_1:10;
thus x in F . k by A2, A3; :: thesis: verum

end;

hence x in meet F by A1, Th19; :: thesis: verum

end;

thus meet F c= lim_inf F by Th7; :: thesis: verum