let x be R_eal; :: thesis: ( 0. < x implies 0. < len x )
assume A1: 0. < x ; :: thesis: 0. < len x
then consider y being R_eal such that
A2: ( 0. < y & y + y < x ) by Th26;
y in Seg x by A1, A2, Def2;
then A3: y <= sup (Seg x) by XXREAL_2:4;

per cases ( y < len x or y = len x ) by A3, XXREAL_0:1;

suppose y < len x ; :: thesis: 0. < len x

hence 0. < len x by A2, XXREAL_0:2; :: thesis: verum

end;

suppose y = len x ; :: thesis: 0. < len x

hence 0. < len x by A2; :: thesis: verum

end;

end;