defpred S_{1}[ 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_{1}[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

( 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

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