let r2, x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL st 0 < r2 & ].(x0 - r2),x0.[ \/ ].x0,(x0 + r2).[ c= dom f holds
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
let f be PartFunc of REAL ,REAL ; :: thesis: ( 0 < r2 & ].(x0 - r2),x0.[ \/ ].x0,(x0 + r2).[ c= dom f implies for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) )
assume A1: ( 0 < r2 & ].(x0 - r2),x0.[ \/ ].x0,(x0 + r2).[ c= dom f ) ; :: thesis: for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
( ].(x0 - r2),x0.[ c= ].(x0 - r2),x0.[ \/ ].x0,(x0 + r2).[ & ].x0,(x0 + r2).[ c= ].(x0 - r2),x0.[ \/ ].x0,(x0 + r2).[ ) by XBOOLE_1:7;
then A2: ( ].(x0 - r2),x0.[ c= dom f & ].x0,(x0 + r2).[ c= dom f ) by A1, XBOOLE_1:1;
let r1, r2 be Real; :: thesis: ( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) )
assume A3: ( r1 < x0 & x0 < r2 ) ; :: thesis: ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
then consider g1 being Real such that
A4: ( r1 < g1 & g1 < x0 & g1 in dom f ) by A1, A2, LIMFUNC2:3;
take g1 ; :: thesis: ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
consider g2 being Real such that
A5: ( g2 < r2 & x0 < g2 & g2 in dom f ) by A1, A2, A3, LIMFUNC2:4;
take g2 ; :: thesis: ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
thus ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) by A4, A5; :: thesis: verum