let a, b be non zero Nat; :: thesis: ( Parity (a + b) < (Parity a) + (Parity b) implies Parity (a + b) = min ((Parity a),(Parity b)) )
assume Parity (a + b) < (Parity a) + (Parity b) ; :: thesis: Parity (a + b) = min ((Parity a),(Parity b))
then Parity a <> Parity b by PEQ;

per cases then ( Parity a > Parity b or Parity a < Parity b ) by XXREAL_0:1;

suppose B1: Parity a > Parity b ; :: thesis: Parity (a + b) = min ((Parity a),(Parity b))

then Parity (a + b) = Parity b by PAP;
hence Parity (a + b) = min ((Parity a),(Parity b)) by B1, XXREAL_0:def 9; :: thesis: verum

end;

suppose B1: Parity a < Parity b ; :: thesis: Parity (a + b) = min ((Parity a),(Parity b))

then Parity (a + b) = Parity a by PAP;
hence Parity (a + b) = min ((Parity a),(Parity b)) by B1, XXREAL_0:def 9; :: thesis: verum

end;

end;