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