defpred S₁[ set ] means ex y being set st [$1,y] in R;
consider X being set such that
A1: for x being set holds
( x in X iff ( x in union (union R) & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff ex y being set st [x,y] in R )
let x be set ; :: thesis: ( x in X iff ex y being set st [x,y] in R )
( ex y being set st [x,y] in R implies x in union (union R) ) by ZFMISC_1:134;
hence ( x in X iff ex y being set st [x,y] in R ) by A1; :: thesis: verum