let a, b be odd Integer; :: thesis: min ((Parity (a - b)),(Parity (a + b))) <= 2
A0: ( |.a.| in NAT & |.b.| in NAT ) by INT_1:3;
then reconsider k = |.a.| as odd Nat ;
reconsider l = |.b.| as odd Nat by A0;

per cases ( k = l or k <> l ) ;

suppose k = l ; :: thesis: min ((Parity (a - b)),(Parity (a + b))) <= 2

then Parity |.(|.a.| - |.b.|).| = 0 by Def1;
then ( Parity |.(a - b).| = 0 or Parity |.(a + b).| = 0 ) by ABS1;
then ( Parity (a - b) = 0 or Parity (a + b) = 0 ) by PMP;
hence min ((Parity (a - b)),(Parity (a + b))) <= 2 by XXREAL_0:def 9; :: thesis: verum

end;

suppose k <> l ; :: thesis: min ((Parity (a - b)),(Parity (a + b))) <= 2

hence min ((Parity (a - b)),(Parity (a + b))) <= 2 by MPO; :: thesis: verum

end;

end;