let F be SetSequence of the carrier of (TOP-REAL 2); :: thesis: for A being Subset of (TOP-REAL 2) st ( for i being Nat holds F . i = A ) holds
Lim_sup F = Cl A
let A be Subset of (TOP-REAL 2); :: thesis: ( ( for i being Nat holds F . i = A ) implies Lim_sup F = Cl A )
assume A1: for i being Nat holds F . i = A ; :: thesis: Lim_sup F = Cl A
then Lim_inf F = Lim_sup F by Th39;
hence Lim_sup F = Cl A by A1, Th23; :: thesis: verum