let a be non zero Integer; :: thesis: Oddity (Parity a) = 1
( Parity (Parity a) = Parity a & (Parity (Parity a)) * (Oddity (Parity a)) = Parity a ) ;
hence Oddity (Parity a) = 1 by XCMPLX_1:7; :: thesis: verum