let X, x, y, z be set ; :: thesis: ( [x,y] in [:NAT ,{X}:] & [x,z] in [:NAT ,{X}:] implies y = z )
assume that
A1: [x,y] in [:NAT ,{X}:] and
A2: [x,z] in [:NAT ,{X}:] ; :: thesis: y = z
y in {X} by A1, ZFMISC_1:106;
then A3: y = X by TARSKI:def 1;
z in {X} by A2, ZFMISC_1:106;
hence y = z by A3, TARSKI:def 1; :: thesis: verum