let x be ext-real number ; :: thesis: ( 0 < x implies ex y being real number st
( 0 < y & y + y < x ) )
assume 0 < x ; :: thesis: ex y being real number st
( 0 < y & y + y < x )
then consider x1 being real number such that
A1: ( 0 < x1 & x1 < x ) by Th23;
consider x2 being real number such that
A2: ( 0 < x2 & x1 + x2 < x ) by A1, Th43;
take y = min x1,x2; :: thesis: ( 0 < y & y + y < x )

per cases ( x1 <= x2 or x2 <= x1 ) ;

suppose A3: x1 <= x2 ; :: thesis: ( 0 < y & y + y < x )

then A4: y = x1 by XXREAL_0:def 9;
thus 0 < y by A1, A3, XXREAL_0:def 9; :: thesis: y + y < x
( y + y <= x1 + x2 & x1 + x2 <= x ) by A2, A3, A4, Th36;
hence y + y < x by A2, XXREAL_0:2; :: thesis: verum

end;

suppose A5: x2 <= x1 ; :: thesis: ( 0 < y & y + y < x )

then A6: y = x2 by XXREAL_0:def 9;
thus 0 < y by A2, A5, XXREAL_0:def 9; :: thesis: y + y < x
( y + y <= x1 + x2 & x1 + x2 <= x ) by A2, A5, A6, Th36;
hence y + y < x by A2, XXREAL_0:2; :: thesis: verum

end;

end;