let x be ExtReal; :: thesis: 0 <= |.x.|
reconsider x = x as R_eal by XXREAL_0:def 1;
0 <= |.x.| ;
hence 0 <= |.x.| ; :: thesis: verum