defpred S1[ object ] means ex i0 being Integer st
( i0 = $1 & P1[i0] );
consider X being set such that
A1:
for y being object holds
( y in X iff ( y in INT & S1[y] ) )
from XBOOLE_0:sch 1();
for y being object st y in X holds
y in INT
by A1;
then reconsider X = X as Subset of INT by TARSKI:def 3;
take
X
; for x being Integer holds
( x in X iff P1[x] )
let i0 be Integer; ( i0 in X iff P1[i0] )
A2:
( i0 in X implies P1[i0] )
proof
assume
i0 in X
;
P1[i0]
then
ex
i1 being
Integer st
(
i0 = i1 &
P1[
i1] )
by A1;
hence
P1[
i0]
;
verum
end;
( P1[i0] implies i0 in X )
by Def2, A1;
hence
( i0 in X iff P1[i0] )
by A2; verum