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

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

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

suppose A4: 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 such that
A5: r1 < g and
A6: g < r1 + r2 by XREAL_1:5;
reconsider g = g as Real ;
take g = g; :: thesis: ( g < r & r1 < g & g in dom f )
thus ( g < r & r1 < g ) by A4, A5, A6, XXREAL_0:2; :: thesis: g in dom f
g in { g2 where g2 is Real : ( r1 < g2 & g2 < r1 + r2 ) } by A5, A6;
then g in ].r1,(r1 + r2).[ 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
( g < r & r1 < g & g in dom f )

consider g being Real such that
A8: r1 < g and
A9: g < r by A3, XREAL_1:5;
reconsider g = g as Real ;
take g = g; :: thesis: ( g < r & r1 < g & g in dom f )
thus ( g < r & r1 < g ) by A8, A9; :: thesis: g in dom f
g < r1 + r2 by A7, A9, XXREAL_0:2;
then g in { g2 where g2 is Real : ( r1 < g2 & g2 < r1 + r2 ) } by A8;
then g in ].r1,(r1 + r2).[ by RCOMP_1:def 2;
hence g in dom f by A2; :: thesis: verum

end;

end;

end;

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