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

per cases ( a = 0 or a <> 0 ) ;

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

hence Parity a <= |.a.| by Def1; :: thesis: verum

end;

suppose a <> 0 ; :: thesis: Parity a <= |.a.|

then Parity |.a.| <= |.a.| by Th3, NAT_D:7;
hence Parity a <= |.a.| by PMP; :: thesis: verum

end;

end;