let T be non empty TopSpace; :: thesis: for A being SetSequence of the carrier of T holds Lim_inf A c= Lim_sup A
let A be SetSequence of the carrier of T; :: thesis: Lim_inf A c= Lim_sup A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim_inf A or x in Lim_sup A )
assume A1: x in Lim_inf A ; :: thesis: x in Lim_sup A
ex K being subsequence of A st x in Lim_inf K
proof
reconsider B = A as subsequence of A by VALUED_0:19;
take B ; :: thesis: x in Lim_inf B
thus x in Lim_inf B by A1; :: thesis: verum
end;
hence x in Lim_sup A by Def2; :: thesis: verum