thus EvenNAT /\ OddNAT c= {} :: according to XBOOLE_0:def 7,XBOOLE_0:def 10 :: thesis: {} c= EvenNAT /\ OddNAT
proof
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;
thus {} c= EvenNAT /\ OddNAT by XBOOLE_1:2; :: thesis: verum