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