let x, z be ext-real number ; :: thesis: ( 0 <= x & x < z implies ex y being real number st
( 0 < y & x + y < z ) )
assume A1:
( 0 <= x & x < z )
; :: thesis: ex y being real number st
( 0 < y & x + y < z )
per cases
( 0 < x or 0 = x )
by A1;
suppose S:
0 < x
;
:: thesis: ex y being real number st
( 0 < y & x + y < z )then A2:
x in REAL
by A1, XXREAL_0:48;
0 < z - x
by A1, Th19, S;
then consider y being
real number such that A3:
(
0 < y &
y < z - x )
by Th23;
take
y
;
:: thesis: ( 0 < y & x + y < z )A4:
x + y <= x + (z - x)
by A3, Th36;
A5:
x + (z - x) = z
by A2, Th44;
x + y <> z
by A2, A3, Th44;
hence
(
0 < y &
x + y < z )
by A3, A4, A5, XXREAL_0:1;
:: thesis: verum end;