defpred S1[ object , object ] means ( $1 = $2 & P1[$2] );
A1:
for x, y, z being object st S1[x,y] & S1[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 F1() & S1[y,x] ) )
from TARSKI:sch 1(A1);
take
X
; for x being object holds
( x in X iff ( x in F1() & P1[x] ) )
let x be object ; ( x in X iff ( x in F1() & P1[x] ) )
thus
( x in X implies ( x in F1() & P1[x] ) )
( x in F1() & P1[x] implies x in X )proof
assume
x in X
;
( x in F1() & P1[x] )
then
ex
y being
object st
(
y in F1() &
S1[
y,
x] )
by A2;
hence
(
x in F1() &
P1[
x] )
;
verum
end;
assume
( x in F1() & P1[x] )
; x in X
then
ex y being object st
( y in F1() & S1[y,x] )
;
hence
x in X
by A2; verum