take X = [:NAT,{0}:]; :: thesis: ( X is infinite & X is disjoint_with_NAT )
thus X is infinite ; :: thesis: X is disjoint_with_NAT
now :: thesis: for x being object st x in X holds
not x in NAT
let x be object ; :: thesis: ( x in X implies not x in NAT )
assume x in X ; :: thesis: not x in NAT
then A1: ex a, b being object 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