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