let r2, r1 be Real; :: thesis: for f being PartFunc of REAL ,REAL st 0 < r2 & ].(r1 - r2),r1.[ c= dom f holds
for r being Real st r < r1 holds
ex g being Real st
( r < g & g < r1 & g in dom f )
let f be PartFunc of REAL ,REAL ; :: thesis: ( 0 < r2 & ].(r1 - r2),r1.[ c= dom f implies for r being Real st r < r1 holds
ex g being Real st
( r < g & g < r1 & g in dom f ) )
assume A1: ( 0 < r2 & ].(r1 - r2),r1.[ c= dom f ) ; :: thesis: for r being Real st r < r1 holds
ex g being Real st
( r < g & g < r1 & g in dom f )
let r be Real; :: thesis: ( r < r1 implies ex g being Real st
( r < g & g < r1 & g in dom f ) )
assume A2: r < r1 ; :: thesis: ex g being Real st
( r < g & g < r1 & g in dom f )

now

per cases ( r1 - r2 <= r or r <= r1 - r2 ) ;

suppose A3: r1 - r2 <= r ; :: thesis: ex g being Real st
( r < g & g < r1 & g in dom f )

consider g being real number such that
A4: ( r < g & g < r1 ) by A2, XREAL_1:7;
reconsider g = g as Real by XREAL_0:def 1;
take g = g; :: thesis: ( r < g & g < r1 & g in dom f )
thus ( r < g & g < r1 ) by A4; :: thesis: g in dom f
r1 - r2 < g by A3, A4, XXREAL_0:2;
then g in { g2 where g2 is Real : ( r1 - r2 < g2 & g2 < r1 ) } by A4;
then g in ].(r1 - r2),r1.[ by RCOMP_1:def 2;
hence g in dom f by A1; :: thesis: verum

end;

suppose A5: r <= r1 - r2 ; :: thesis: ex g being Real st
( r < g & g < r1 & g in dom f )

r1 - r2 < r1 by A1, Lm1;
then consider g being real number such that
A6: ( r1 - r2 < g & g < r1 ) by XREAL_1:7;
reconsider g = g as Real by XREAL_0:def 1;
take g = g; :: thesis: ( r < g & g < r1 & g in dom f )
thus ( r < g & g < r1 ) by A5, A6, XXREAL_0:2; :: thesis: g in dom f
g in { g2 where g2 is Real : ( r1 - r2 < g2 & g2 < r1 ) } by A6;
then g in ].(r1 - r2),r1.[ by RCOMP_1:def 2;
hence g in dom f by A1; :: thesis: verum

end;

end;

end;

hence ex g being Real st
( r < g & g < r1 & g in dom f ) ; :: thesis: verum