let x1, x2 be Subset of [:NAT,NAT:]; ( ( for x being Element of [:NAT,NAT:] holds
( x in x1 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) ) ) & ( for x being Element of [:NAT,NAT:] holds
( x in x2 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) ) ) implies x1 = x2 )
assume that
A1:
for x being Element of [:NAT,NAT:] holds
( x in x1 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) )
and
A2:
for x being Element of [:NAT,NAT:] holds
( x in x2 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) )
; x1 = x2
x1 = x2
hence
x1 = x2
; verum