defpred S₁[ object , object ] means ( $1 = $2 & P₁[$2] );
A1: for x, y, z being object st S₁[x,y] & S₁[x,z] holds
y = z ;
consider X being set such that
A2: for x being object holds
( x in X iff ex y being object st
( y in F₁() & S₁[y,x] ) ) from TARSKI:sch 1(A1);
take X ; :: thesis: for x being object holds
( x in X iff ( x in F₁() & P₁[x] ) )
let x be object ; :: thesis: ( x in X iff ( x in F₁() & P₁[x] ) )
thus ( x in X implies ( x in F₁() & P₁[x] ) ) :: thesis: ( x in F₁() & P₁[x] implies x in X )

proof

assume x in X ; :: thesis: ( x in F₁() & P₁[x] )
then ex y being object st
( y in F₁() & S₁[y,x] ) by A2;
hence ( x in F₁() & P₁[x] ) ; :: thesis: verum

end;

assume ( x in F₁() & P₁[x] ) ; :: thesis: x in X
then ex y being object st
( y in F₁() & S₁[y,x] ) ;
hence x in X by A2; :: thesis: verum