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