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 that
A1: P is Bounded and
A2: for i being Element of NAT holds S . i c= P ; :: thesis: Lim_inf S is compact
Lim_inf S is Bounded by A1, A2, Th62;
hence Lim_inf S is compact by Th52, TOPREAL6:88; :: thesis: verum