let x be R_eal; :: thesis: ( |.x.| < +infty iff x in REAL )
thus ( |.x.| < +infty implies x in REAL ) by Th67, XXREAL_0:14; :: thesis: ( x in REAL implies |.x.| < +infty )
assume A1: x in REAL ; :: thesis: |.x.| < +infty
assume |.x.| >= +infty ; :: thesis: contradiction
hence contradiction by A1, Th101, XXREAL_0:4; :: thesis: verum