let x be R_eal; :: thesis: ( 0. < x implies len x <= x )
assume A1: 0. < x ; :: thesis: len x <= x
for y being ext-real number st y in Seg x holds
y <= x

proof

let y be ext-real number ; :: thesis: ( y in Seg x implies y <= x )
assume A2: y in Seg x ; :: thesis: y <= x
reconsider y = y as R_eal by XXREAL_0:def 1;
( 0. < y & y + y < x ) by A1, A2, Def2;
hence y <= x by Th22; :: thesis: verum

end;

then x is UpperBound of Seg x by XXREAL_2:def 1;
hence len x <= x by XXREAL_2:def 3; :: thesis: verum