defpred S₁[ object ] means ex f being Function of S,BOOLEAN st
( f = $1 & f . s = TRUE );
consider IT being set such that
A1: for x being object holds
( x in IT iff ( x in X & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being object st x in IT holds
x in X by A1;
then reconsider IT = IT as Subset of X by TARSKI:def 3;
take IT ; :: thesis: for x being object holds
( x in IT iff ( x in X & ex f being Function of S,BOOLEAN st
( f = x & f . s = TRUE ) ) )
thus for x being object holds
( x in IT iff ( x in X & ex f being Function of S,BOOLEAN st
( f = x & f . s = TRUE ) ) ) by A1; :: thesis: verum