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

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