let a, b be odd Integer; :: thesis: ( |.a.| <> |.b.| implies min ((Parity (a - b)),(Parity (a + b))) = 2 )
assume A1: |.a.| <> |.b.| ; :: 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;
( k - l <> 0 & k + l <> 0 ) by A1;
then A2: ( Parity (k - l) = 2 |^ (2 |-count (k - l)) & Parity (k + l) = 2 |^ (2 |-count (k + l)) ) by Def1;
A3: ( Parity (k - l) = Parity |.(k - l).| & Parity (a + b) = Parity |.(a + b).| & Parity (a - b) = Parity |.(a - b).| ) by PMP;
min ((2 |-count (k - l)),(2 |-count (k + l))) = 1 by A1, NEWTON03:82;
then A4: min ((Parity (k - l)),(Parity (k + l))) = 2 |^ 1 by A2, MIN1;

per cases ( |.(a + b).| = |.a.| + |.b.| or |.(a - b).| = |.a.| + |.b.| ) by ABS;

suppose |.(a + b).| = |.a.| + |.b.| ; :: thesis: min ((Parity (a - b)),(Parity (a + b))) = 2

then |.(a - (- b)).| = |.a.| + |.(- b).| by COMPLEX1:52;
then ( |.(a - (- b)).| = |.a.| + |.(- b).| & |.(a + (- b)).| = |.(|.a.| - |.(- b).|).| ) by LmABS;
then ( Parity |.(a + b).| = Parity (|.a.| + |.b.|) & Parity |.(a - b).| = Parity |.(|.a.| - |.b.|).| ) by COMPLEX1:52;
hence min ((Parity (a - b)),(Parity (a + b))) = 2 by A4, A3; :: thesis: verum

end;

suppose |.(a - b).| = |.a.| + |.b.| ; :: thesis: min ((Parity (a - b)),(Parity (a + b))) = 2

hence min ((Parity (a - b)),(Parity (a + b))) = 2 by A4, A3, LmABS; :: thesis: verum

end;

end;