defpred S₁[ object ] means ex A being subsequence of S st $1 in Lim_inf A;
consider X being set such that
A1: for x being object holds
( x in X iff ( x in the carrier of T & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= the carrier of T by A1;
then reconsider X = X as Subset of T ;
take X ; :: thesis: for x being object holds
( x in X iff ex A being subsequence of S st x in Lim_inf A )
thus for x being object holds
( x in X iff ex A being subsequence of S st x in Lim_inf A ) by A1; :: thesis: verum