defpred S₁[ object ] means ex x, y being set st
( x in X & y in X & $1 = {x,y} );
consider S being set such that
A1: for z being object holds
( z in S iff ( z in bool X & S₁[z] ) ) from XBOOLE_0:sch 1();
take S ; :: thesis: for z being set holds
( z in S iff ex x, y being set st
( x in X & y in X & z = {x,y} ) )
let z be set ; :: thesis: ( z in S iff ex x, y being set st
( x in X & y in X & z = {x,y} ) )
thus ( z in S implies S₁[z] ) by A1; :: thesis: ( ex x, y being set st
( x in X & y in X & z = {x,y} ) implies z in S )
assume A2: S₁[z] ; :: thesis: z in S
then z c= X by ZFMISC_1:32;
hence z in S by A1, A2; :: thesis: verum