thus EvenNAT \/ OddNAT c= NAT ; :: according to XBOOLE_0:def 10 :: thesis: NAT c= EvenNAT \/ OddNAT
let n be object ; :: according to TARSKI:def 3 :: thesis: ( not n in NAT or n in EvenNAT \/ OddNAT )
assume A1: ( n in NAT & not n in EvenNAT \/ OddNAT ) ; :: thesis: contradiction
then reconsider n = n as Nat ;
( n in NAT & not n in EvenNAT & not n in OddNAT ) by A1, XBOOLE_0:def 3;
then ( not n is even & not n is odd ) ;
hence contradiction ; :: thesis: verum