let X be set ; :: thesis: ( ( for p being set st p in [:NAT ,{X}:] holds
ex x, y being set st [x,y] = p ) & ( for x, y, z being set st [x,y] in [:NAT ,{X}:] & [x,z] in [:NAT ,{X}:] holds
y = z ) )
for x, y, z being set st [x,y] in [:NAT ,{X}:] & [x,z] in [:NAT ,{X}:] holds
y = z

proof

let 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

end;

hence ( ( for p being set st p in [:NAT ,{X}:] holds
ex x, y being set st [x,y] = p ) & ( for x, y, z being set st [x,y] in [:NAT ,{X}:] & [x,z] in [:NAT ,{X}:] holds
y = z ) ) by RELAT_1:def 1; :: thesis: verum