let x be R_eal; :: thesis: ( not |.x.| = +infty or x = +infty or x = -infty )
assume A1: |.x.| = +infty ; :: thesis: ( x = +infty or x = -infty )
( |.x.| = x or - |.x.| = - (- x) ) by EXTREAL1:def 3;
hence ( x = +infty or x = -infty ) by A1, XXREAL_3:5; :: thesis: verum