take X = [:NAT ,{0 }:]; :: thesis: ( not X is finite & X is disjoint_with_NAT )
thus not X is finite ; :: thesis: X is disjoint_with_NAT

now

let x be set ; :: thesis: ( x in X implies not x in NAT )
assume x in X ; :: thesis: not x in NAT
then A1: ex a, b being set st
( a in NAT & b in {0 } & x = [a,b] ) by ZFMISC_1:def 2;
assume x in NAT ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum

end;

hence X misses NAT by XBOOLE_0:3; :: according to FREEALG:def 1 :: thesis: verum