now

let z be set ; :: thesis: ( z in [:A,B:] implies not z in NAT )
assume ( z in [:A,B:] & z in NAT ) ; :: thesis: contradiction
then ( z is Element of NAT & ex a, b being set st
( a in A & b in B & z = [a,b] ) ) by ZFMISC_1:def 2;
hence contradiction ; :: thesis: verum

end;

hence [:A,B:] misses NAT by XBOOLE_0:3; :: according to FREEALG:def 1 :: thesis: verum