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 set ; :: 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 Element of NAT such that
A2: for k being Element of NAT holds x in F . (n + k) by Th7;
ex k being Element of NAT st
for n being Element of NAT st n > k holds
x in F . n

proof

take k = n; :: thesis: for n being Element of NAT st n > k holds
x in F . n
let n be Element of NAT ; :: thesis: ( n > k implies x in F . n )
assume n > k ; :: thesis: x in F . n
then consider h being Nat such that
A3: n = k + h by NAT_1:10;
h in NAT by ORDINAL1:def 13;
hence x in F . n by A2, A3; :: thesis: verum

end;

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

end;

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