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

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

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

end;

end;

end;

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