defpred S₁[ object ] means ex p being XFinSequence st
( P₁[p] & $1 = p );
consider Y being set such that
A1: for x being object holds
( x in Y iff ( x in F₁() ^omega & S₁[x] ) ) from XBOOLE_0:sch 1();
take Y ; :: thesis: for x being object holds
( x in Y iff ex p being XFinSequence st
( p in F₁() ^omega & P₁[p] & x = p ) )
for x being object st x in Y holds
ex p being XFinSequence st
( p in F₁() ^omega & P₁[p] & x = p )

proof

let x be object ; :: thesis: ( x in Y implies ex p being XFinSequence st
( p in F₁() ^omega & P₁[p] & x = p ) )
assume x in Y ; :: thesis: ex p being XFinSequence st
( p in F₁() ^omega & P₁[p] & x = p )
then ( x in F₁() ^omega & ex p being XFinSequence st
( P₁[p] & x = p ) ) by A1;
hence ex p being XFinSequence st
( p in F₁() ^omega & P₁[p] & x = p ) ; :: thesis: verum

end;

hence for x being object holds
( x in Y iff ex p being XFinSequence st
( p in F₁() ^omega & P₁[p] & x = p ) ) by A1; :: thesis: verum