let x be R_eal; :: thesis: ( 0. < x implies (len x) + (len x) <= x )
assume A1: 0. < x ; :: thesis: (len x) + (len x) <= x
A2: ( x in REAL or x in {-infty ,+infty } ) by XBOOLE_0:def 3, XXREAL_0:def 4;

per cases ( x is Real or x = +infty ) by A1, A2, SUPINF_2:19, TARSKI:def 2;

suppose A3: x is Real ; :: thesis: (len x) + (len x) <= x

assume not (len x) + (len x) <= x ; :: thesis: contradiction
then consider eps being R_eal such that
A4: ( 0. < eps & x + eps < (len x) + (len x) & eps in REAL ) by A1, Th24;
consider eps0 being R_eal such that
A5: ( 0. < eps0 & eps0 + eps0 < eps ) by A4, Th26;
A6: x < +infty by A3, XXREAL_0:4;
A7: ( 0. < eps0 & eps0 <= eps & eps in REAL ) by A4, A5, Th22;
then A8: eps0 is Real by XXREAL_0:47;
reconsider a = len x, b = eps0 as Real by A1, A6, A7, Th29, XXREAL_0:47;
A9: (len x) - eps0 = a - b by SUPINF_2:5;
a + 0 <= a + b by A5, XREAL_1:9;
then A10: (len x) - eps0 <= len x by A9, XREAL_1:22;
A11: a - b <> a by A5;
ex y being ext-real number st
( y in Seg x & not y <= (len x) - eps0 )

proof

assume for y being ext-real number st y in Seg x holds
y <= (len x) - eps0 ; :: thesis: contradiction
then (len x) - eps0 is UpperBound of Seg x by XXREAL_2:def 1;
then sup (Seg x) <= (len x) - eps0 by XXREAL_2:def 3;
hence contradiction by A9, A10, A11, XXREAL_0:1; :: thesis: verum

end;

then consider y being R_eal such that
A12: ( y in Seg x & (len x) - eps0 <= y ) ;
A13: ( 0. < y & y + y < x & (len x) - eps0 <= y ) by A1, A12, Def2;
((len x) - eps0) + eps0 <= y + eps0 by A8, A12, Th11;
then A14: len x <= y + eps0 by A8, Th8;
0. < len x by A1, Th27;
then A15: (len x) + (len x) <= (y + eps0) + (y + eps0) by A14, MEASURE1:4;
A16: ( 0. <= y & 0. <= eps0 ) by A1, A5, A12, Def2;
then A17: 0. + 0. <= y + eps0 by MEASURE1:4;
A18: 0. + 0. = 0. by SUPINF_2:18;
then A19: 0. <= y + y by A16, MEASURE1:4;
A20: 0. <= eps0 + eps0 by A5, A18, MEASURE1:4;
(y + eps0) + (y + eps0) = y + (eps0 + (y + eps0)) by A16, A17, A18, MEASURE4:1
.= y + (y + (eps0 + eps0)) by A16, MEASURE4:1
.= (y + y) + (eps0 + eps0) by A16, A20, MEASURE4:1 ;
then (y + eps0) + (y + eps0) <= x + eps by A5, A13, A19, A20, MEASURE1:4;
hence contradiction by A4, A15, XXREAL_0:2; :: thesis: verum

end;

suppose A21: x = +infty ; :: thesis: (len x) + (len x) <= x

A22: len x <= x by A1, Th28;
(len x) + (len x) <= x + x by A22, SUPINF_2:14;
hence (len x) + (len x) <= x by A21, SUPINF_2:def 2; :: thesis: verum

end;

end;