defpred S₁[ object ] means ex a being set st
( a in X . i & $1 = [a,i] );
consider A being set such that
A2: for x being object holds
( x in A iff ( x in [:(X . i),I:] & S₁[x] ) ) from XBOOLE_0:sch 1();
take A ; :: thesis: for x being set holds
( x in A iff ex a being set st
( a in X . i & x = [a,i] ) )
let x be set ; :: thesis: ( x in A iff ex a being set st
( a in X . i & x = [a,i] ) )
thus ( x in A implies ex a being set st
( a in X . i & x = [a,i] ) ) by A2; :: thesis: ( ex a being set st
( a in X . i & x = [a,i] ) implies x in A )
given a being set such that A3: ( a in X . i & x = [a,i] ) ; :: thesis: x in A
x in [:(X . i),I:] by A1, A3, ZFMISC_1:87;
hence x in A by A2, A3; :: thesis: verum