let S be SetSequence of the carrier of (TOP-REAL 2); :: thesis: for P being Subset of (TOP-REAL 2) st P is Bounded & ( for i being Element of NAT holds S . i c= P ) holds
Lim_inf S is compact
let P be Subset of (TOP-REAL 2); :: thesis: ( P is Bounded & ( for i being Element of NAT holds S . i c= P ) implies Lim_inf S is compact )
assume ( P is Bounded & ( for i being Element of NAT holds S . i c= P ) ) ; :: thesis: Lim_inf S is compact
then Lim_inf S is Bounded by Th60;
hence Lim_inf S is compact by TOPREAL6:79; :: thesis: verum