now :: thesis: for z being object st z in [:A,B:] holds
not z in NAT
let z be object ; :: thesis: ( z in [:A,B:] implies not z in NAT )
assume that
A1: z in [:A,B:] and
A2: z in NAT ; :: thesis: contradiction
ex a, b being object st
( a in A & b in B & z = [a,b] ) by A1, ZFMISC_1:def 2;
hence contradiction by A2; :: thesis: verum
end;
hence [:A,B:] misses NAT by XBOOLE_0:3; :: according to FREEALG:def 1 :: thesis: verum