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