let x be R_eal; :: thesis: ( 0. < x & x < +infty implies len x is Real )
assume A1: ( 0. < x & x < +infty ) ; :: thesis: len x is Real
then ( 0. < len x & len x <= x ) by Th27, Th28;
then ( 0. < len x & len x < +infty ) by A1, XXREAL_0:2;
hence len x is Real by XXREAL_0:48; :: thesis: verum