defpred S₁[ object ] means ex A being subsequence of S st $1 in Lim_inf A;
let A1, A2 be Subset of T; :: thesis: ( ( for x being object holds
( x in A1 iff ex A being subsequence of S st x in Lim_inf A ) ) & ( for x being object holds
( x in A2 iff ex A being subsequence of S st x in Lim_inf A ) ) implies A1 = A2 )
assume that
A2: for x being object holds
( x in A1 iff S₁[x] ) and
A3: for x being object holds
( x in A2 iff S₁[x] ) ; :: thesis: A1 = A2
A1 = A2 from XBOOLE_0:sch 2(A2, A3);
hence A1 = A2 ; :: thesis: verum