for A, B being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Nat holds A . i c= B . i ) holds
Lim_sup A c= Lim_sup B