thus
EvenNAT /\ OddNAT c= {}
:: according to XBOOLE_0:def 7,XBOOLE_0:def 10 :: thesis: {} c= EvenNAT /\ OddNAT

proof

thus
{} c= EvenNAT /\ OddNAT
by XBOOLE_1:2; :: thesis: verum
let n be object ; :: according to TARSKI:def 3 :: thesis: ( not n in EvenNAT /\ OddNAT or n in {} )

assume n in EvenNAT /\ OddNAT ; :: thesis: n in {}

then A1: ( n in EvenNAT & n in OddNAT ) by XBOOLE_0:def 4;

consider e being Nat such that

A2: ( e = n & e is even ) by A1;

consider o being Nat such that

A3: ( o = n & o is odd ) by A1;

thus n in {} by A2, A3; :: thesis: verum

end;assume n in EvenNAT /\ OddNAT ; :: thesis: n in {}

then A1: ( n in EvenNAT & n in OddNAT ) by XBOOLE_0:def 4;

consider e being Nat such that

A2: ( e = n & e is even ) by A1;

consider o being Nat such that

A3: ( o = n & o is odd ) by A1;

thus n in {} by A2, A3; :: thesis: verum