defpred S₁[ set ] means ex S being Subset of X st
( S = $1 & S is f -closed );
consider Y being Subset of (bool X) such that
A1: for x being set holds
( x in Y iff ( x in bool X & S₁[x] ) ) from SUBSET_1:sch 1();
take Y ; :: thesis: for x being object holds
( x in Y iff ex S being Subset of X st
( S = x & S is f -closed ) )
thus for x being object holds
( x in Y iff ex S being Subset of X st
( S = x & S is f -closed ) ) by A1; :: thesis: verum