defpred S₁[ set ] means ex x being set st
( [x,$1] in R & x in X );
consider Y being set such that
A1: for y being set holds
( y in Y iff ( y in rng R & S₁[y] ) ) from XBOOLE_0:sch 1();
take Y ; :: thesis: for y being set holds
( y in Y iff ex x being set st
( [x,y] in R & x in X ) )
let y be set ; :: thesis: ( y in Y iff ex x being set st
( [x,y] in R & x in X ) )
thus ( y in Y implies ex x being set st
( [x,y] in R & x in X ) ) by A1; :: thesis: ( ex x being set st
( [x,y] in R & x in X ) implies y in Y )
given x being set such that A2: [x,y] in R and
A3: x in X ; :: thesis: y in Y
y in rng R by A2, Def5;
hence y in Y by A1, A2, A3; :: thesis: verum