let r1, r2 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 that
A1: 0 < r2 and
A2: ].(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 A3: r < r1 ; :: thesis: ex g being Real st
( r < g & g < r1 & g in dom f )

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

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

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

consider g being Real such that
A5: r < g and
A6: g < r1 by A3, XREAL_1:5;
reconsider g = g as Real ;
take g = g; :: thesis: ( r < g & g < r1 & g in dom f )
thus ( r < g & g < r1 ) by A5, A6; :: thesis: g in dom f
r1 - r2 < g by A4, A5, XXREAL_0:2;
then 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 A2; :: thesis: verum

end;

suppose A7: 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 such that
A8: r1 - r2 < g and
A9: g < r1 by XREAL_1:5;
reconsider g = g as Real ;
take g = g; :: thesis: ( r < g & g < r1 & g in dom f )
thus ( r < g & g < r1 ) by A7, A8, A9, XXREAL_0:2; :: thesis: g in dom f
g in { g2 where g2 is Real : ( r1 - r2 < g2 & g2 < r1 ) } by A8, A9;
then g in ].(r1 - r2),r1.[ by RCOMP_1:def 2;
hence g in dom f by A2; :: thesis: verum

end;

end;

end;

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