let A, B be SetSequence of the carrier of (TOP-REAL 2); :: thesis: ( ( for i being Nat holds A . i c= B . i ) implies Lim_sup A c= Lim_sup B )
assume A1: for i being Nat holds A . i c= B . i ; :: thesis: Lim_sup A c= Lim_sup B
Lim_sup A c= Lim_sup B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim_sup A or x in Lim_sup B )
assume x in Lim_sup A ; :: thesis: x in Lim_sup B
then consider A1 being subsequence of A such that
A2: x in Lim_inf A1 by Def2;
consider D being subsequence of B such that
A3: for i being Nat holds A1 . i c= D . i by A1, Th32;
Lim_inf A1 c= Lim_inf D by A3, Th17;
hence x in Lim_sup B by A2, Def2; :: thesis: verum
end;
hence Lim_sup A c= Lim_sup B ; :: thesis: verum