let x be set ; :: thesis: ( x in [:NAT,NAT:] implies ex n1, n2 being Element of NAT st x = [n1,n2] )

assume A1: x in [:NAT,NAT:] ; :: thesis: ex n1, n2 being Element of NAT st x = [n1,n2]

then reconsider n1 = x `1 , n2 = x `2 as Element of NAT by MCART_1:10;

take n1 ; :: thesis: ex n2 being Element of NAT st x = [n1,n2]

take n2 ; :: thesis: x = [n1,n2]

thus x = [n1,n2] by A1, MCART_1:21; :: thesis: verum

assume A1: x in [:NAT,NAT:] ; :: thesis: ex n1, n2 being Element of NAT st x = [n1,n2]

then reconsider n1 = x `1 , n2 = x `2 as Element of NAT by MCART_1:10;

take n1 ; :: thesis: ex n2 being Element of NAT st x = [n1,n2]

take n2 ; :: thesis: x = [n1,n2]

thus x = [n1,n2] by A1, MCART_1:21; :: thesis: verum