defpred S1[ object , object ] means GO $1,$2;
A1: for x, y1, y2 being object st S1[x,y1] & S1[x,y2] holds
y1 = y2 by Th15;
consider Y being set such that
A2: for y being object holds
( y in Y iff ex x being object st
( x in UN & S1[x,y] ) ) from TARSKI:sch 1(A1);
 take Y ; :: thesis: for y being object holds
( y in Y iff ex x being set st
( x in UN & GO x,y ) )
let y be object ; :: thesis: ( y in Y iff ex x being set st
( x in UN & GO x,y ) )
thus ( y in Y implies ex x being set st
( x in UN & GO x,y ) ) :: thesis: ( ex x being set st
( x in UN & GO x,y ) implies y in Y )
proof
assume y in Y ; :: thesis: ex x being set st
( x in UN & GO x,y )
then ex x being object st
( x in UN & S1[x,y] ) by A2;
hence ex x being set st
( x in UN & GO x,y ) ; :: thesis: verum
end;
thus ( ex x being set st
( x in UN & GO x,y ) implies y in Y ) by A2; :: thesis: verum