take X = {(- 1)}; :: thesis: ( not X is empty & X is disjoint_with_NAT )
thus not X is empty ; :: thesis: X is disjoint_with_NAT

now

assume X meets NAT ; :: thesis: contradiction
then consider x being set such that
A1: ( x in X & x in NAT ) by XBOOLE_0:3;
reconsider x = x as Element of NAT by A1;
( x = - 1 & 0 <= x ) by A1, NAT_1:2, TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

hence X is disjoint_with_NAT by Def1; :: thesis: verum