set X = NAT null ([:{0},NAT:] \ {[0,0]});
reconsider XX = NAT null ([:{0},NAT:] \ {[0,0]}) as Subset of INT ;
XX \ INT = {} ;
hence NAT \ INT is empty ; :: thesis: verum