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