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 :: thesis: not X meets NAT
assume X meets NAT ; :: thesis: contradiction
then consider x being object such that
A1: x in X and
A2: x in NAT by XBOOLE_0:3;
reconsider x = x as Nat by A2;
x = - 1 by A1, TARSKI:def 1;
hence contradiction by NAT_1:2; :: thesis: verum
end;
hence X is disjoint_with_NAT ; :: thesis: verum