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 that
A1: 0 < r2 and
A2: ].(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 )
A3: ].(x0 - r2),x0.[ c= ].(x0 - r2),x0.[ \/ ].x0,(x0 + r2).[ by XBOOLE_1:7;
A4: ].x0,(x0 + r2).[ c= ].(x0 - r2),x0.[ \/ ].x0,(x0 + r2).[ by XBOOLE_1:7;
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 that
A5: r1 < x0 and
A6: 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 )
consider g1 being Real such that
A7: r1 < g1 and
A8: g1 < x0 and
A9: g1 in dom f by A1, A2, A3, A5, LIMFUNC2:3, XBOOLE_1:1;
consider g2 being Real such that
A10: g2 < r2 and
A11: x0 < g2 and
A12: g2 in dom f by A1, A2, A4, A6, LIMFUNC2:4, XBOOLE_1:1;
take g1 ; :: thesis: ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
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 A7, A8, A9, A10, A11, A12; :: thesis: verum