let T be non empty TopSpace; :: thesis: for F being SetSequence of the carrier of T
for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Lim_sup F
let F be SetSequence of the carrier of T; :: thesis: for A being Subset of T st ( for i being Nat holds F . i = A ) holds
Lim_inf F = Lim_sup F
let A be Subset of T; :: thesis: ( ( for i being Nat holds F . i = A ) implies Lim_inf F = Lim_sup F )
assume A1: for i being Nat holds F . i = A ; :: thesis: Lim_inf F = Lim_sup F
thus Lim_inf F c= Lim_sup F by Th31; :: according to XBOOLE_0:def 10 :: thesis: Lim_sup F c= Lim_inf F
thus Lim_sup F c= Lim_inf F :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim_sup F or x in Lim_inf F )
assume x in Lim_sup F ; :: thesis: x in Lim_inf F
then ex G being subsequence of F st x in Lim_inf G by Def2;
hence x in Lim_inf F by A1, Th12; :: thesis: verum
end;