let x be ExtReal; :: thesis: ( x <> 0 implies 0 < |.x.| )
assume A1: x <> 0 ; :: thesis: 0 < |.x.|

per cases ( 0 <= x or not 0 <= x ) ;

suppose 0 <= x ; :: thesis: 0 < |.x.|

hence 0 < |.x.| by A1, Def1; :: thesis: verum

end;

suppose A2: not 0 <= x ; :: thesis: 0 < |.x.|

then 0 < - x ;
hence 0 < |.x.| by A2, Def1; :: thesis: verum

end;

end;