defpred S₁[ object ] means ex y being object st [y,$1] in X;
consider Y being set such that
A5: 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 [y,x] in X )
let x be object ; :: thesis: ( x in Y iff ex y being object st [y,x] in X )
thus ( x in Y implies ex y being object st [y,x] in X ) by A5; :: thesis: ( ex y being object st [y,x] in X implies x in Y )
given y being object such that A6: [y,x] in X ; :: thesis: x in Y
x in union (union X) by A6, Th7;
hence x in Y by A6, A5; :: thesis: verum