let Y1, Y2 be set ; ( ( for y being object holds
( y in Y1 iff ex x being set st
( x in UN & GO x,y ) ) ) & ( for y being object holds
( y in Y2 iff ex x being set st
( x in UN & GO x,y ) ) ) implies Y1 = Y2 )
assume that
A3:
for y being object holds
( y in Y1 iff ex x being set st
( x in UN & GO x,y ) )
and
A4:
for y being object holds
( y in Y2 iff ex x being set st
( x in UN & GO x,y ) )
; Y1 = Y2
now for y being object holds
( y in Y1 iff y in Y2 )let y be
object ;
( y in Y1 iff y in Y2 )
(
y in Y1 iff ex
x being
set st
(
x in UN &
GO x,
y ) )
by A3;
hence
(
y in Y1 iff
y in Y2 )
by A4;
verum end;
hence
Y1 = Y2
by TARSKI:2; verum