let x be ExtReal; :: thesis: ( 0 < x implies ex y being Real st
( 0 < y & y + y < x ) )
assume 0 < x ; :: thesis: ex y being Real st
( 0 < y & y + y < x )
then consider x1 being Real such that
A1: 0 < x1 and
A2: x1 < x by Th3;
consider x2 being Real such that
A3: 0 < x2 and
A4: x1 + x2 < x by A1, A2, Th49;
take y = min (x1,x2); :: thesis: ( 0 < y & y + y < x )
per cases ( x1 <= x2 or x2 <= x1 ) ;
suppose A5: x1 <= x2 ; :: thesis: ( 0 < y & y + y < x )
hence 0 < y by A1, XXREAL_0:def 9; :: thesis: y + y < x
y = x1 by A5, XXREAL_0:def 9;
then y + y <= x1 + x2 by A5, Th36;
hence y + y < x by A4, XXREAL_0:2; :: thesis: verum
end;
suppose A6: x2 <= x1 ; :: thesis: ( 0 < y & y + y < x )
hence 0 < y by A3, XXREAL_0:def 9; :: thesis: y + y < x
y = x2 by A6, XXREAL_0:def 9;
then y + y <= x1 + x2 by A6, Th36;
hence y + y < x by A4, XXREAL_0:2; :: thesis: verum
end;
end;