let a be Integer; :: thesis: Parity a = Parity |.a.|

per cases ( |.a.| = a or |.a.| = - a ) by ABSVALUE:1;

suppose |.a.| = a ; :: thesis: Parity a = Parity |.a.|

hence Parity a = Parity |.a.| ; :: thesis: verum

end;

suppose |.a.| = - a ; :: thesis: Parity a = Parity |.a.|

hence Parity a = Parity |.a.| by PM; :: thesis: verum

end;

end;