defpred S₁[ set , set ] means GO $1,$2,R;
set N = { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum } ;
A1: for x, y1, y2 being set st S₁[x,y1] & S₁[x,y2] holds
y1 = y2 by Th6;
consider Y being set such that
A2: for y being set holds
( y in Y iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum } & S₁[x,y] ) ) from TARSKI:sch 1(A1);
take Y ; :: thesis: for y being set holds
( y in Y iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum } & GO x,y,R ) )
thus for y being set holds
( y in Y iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum } & GO x,y,R ) ) by A2; :: thesis: verum