let x be R_eal; :: thesis: 0 <= |.x.|

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

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

hence 0 <= |.x.| by EXTREAL1:def 3; :: thesis: verum

end;

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

then |.x.| = - x by EXTREAL1:def 3;
hence 0 <= |.x.| by A1; :: thesis: verum

end;

end;