let x0 be Real; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
thus ( ( 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 ) ) implies ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) ) ) :: thesis:

proof

assume A1: 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 ) ; :: thesis:
thus for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) :: thesis:

proof

A2: x0 < x0 + 1 by Lm1;
let r be Real; :: thesis:
assume r < x0 ; :: thesis:
then consider g1, g2 being Real such that
A3: r < g1 and
A4: g1 < x0 and
A5: g1 in dom f and
g2 < x0 + 1 and
x0 < g2 and
g2 in dom f by A1, A2;
take g1 ; :: thesis:
thus ( r < g1 & g1 < x0 & g1 in dom f ) by A3, A4, A5; :: thesis:

end;

A6: x0 - 1 < x0 by Lm1;
let r be Real; :: thesis:
assume x0 < r ; :: thesis:
then consider g1, g2 being Real such that
x0 - 1 < g1 and
g1 < x0 and
g1 in dom f and
A7: g2 < r and
A8: x0 < g2 and
A9: g2 in dom f by A1, A6;
take g2 ; :: thesis:
thus ( g2 < r & x0 < g2 & g2 in dom f ) by A7, A8, A9; :: thesis:

end;

assume that
A10: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) and
A11: for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ; :: thesis:
let r1, r2 be Real; :: thesis:
assume that
A12: r1 < x0 and
A13: x0 < r2 ; :: thesis:
consider g2 being Real such that
A14: g2 < r2 and
A15: x0 < g2 and
A16: g2 in dom f by A11, A13;
consider g1 being Real such that
A17: r1 < g1 and
A18: g1 < x0 and
A19: g1 in dom f by A10, A12;
take g1 ; :: thesis:
take g2 ; :: thesis:
thus ( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) by A17, A18, A19, A14, A15, A16; :: thesis: