defpred S₁[ set ] means ex x being set st [x,$1] in R;
consider Y being set such that
A1: for y being set holds
( y in Y iff ( y in union (union 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 )
let y be set ; :: thesis: ( y in Y iff ex x being set st [x,y] in R )
( ex x being set st [x,y] in R implies y in union (union R) ) by Lm1;
hence ( y in Y iff ex x being set st [x,y] in R ) by A1; :: thesis: verum