defpred S₁[ set ] means ex f being Function st
( $1 = f & dom f c= X & rng f c= Y );
consider F being set such that
A1: for z being set holds
( z in F iff ( z in bool [:X,Y:] & S₁[z] ) ) from XBOOLE_0:sch 1();
take F ; :: thesis: for x being set holds
( x in F iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) )
let z be set ; :: thesis: ( z in F iff ex f being Function st
( z = f & dom f c= X & rng f c= Y ) )
thus ( z in F implies ex f being Function st
( z = f & dom f c= X & rng f c= Y ) ) by A1; :: thesis: ( ex f being Function st
( z = f & dom f c= X & rng f c= Y ) implies z in F )
given f being Function such that A2: z = f and
A3: ( dom f c= X & rng f c= Y ) ; :: thesis: z in F
f c= [:X,Y:]

proof

let x be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in f or [x,b₁] in [:X,Y:] )
let y be set ; :: thesis: ( not [x,y] in f or [x,y] in [:X,Y:] )
assume A4: [x,y] in f ; :: thesis: [x,y] in [:X,Y:]
then A5: x in dom f by RELAT_1:def 4;
then y = f . x by A4, FUNCT_1:def 4;
then y in rng f by A5, FUNCT_1:def 5;
hence [x,y] in [:X,Y:] by A3, A5, ZFMISC_1:def 2; :: thesis: verum

end;

hence z in F by A1, A2, A3; :: thesis: verum