let x be ExtReal; ( 0 < x implies ex y being Real st
( 0 < y & y + y < x ) )
assume
0 < x
; 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); ( 0 < y & y + y < x )