theorem :: KURATO_2:41

for F, G being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Nat holds G . i = Cl (F . i) ) holds
Lim_sup G = Lim_sup F