let x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL 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 ) ) iff ( ( 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 ) ) ) )
let f be PartFunc of REAL ,REAL ; :: 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 ) ) iff ( ( 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 ) ) ) )
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: ( ( 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 ) ) 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 ) )

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

proof

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

end;

let r be Real; :: thesis: ( x0 < r implies ex g being Real st
( g < r & x0 < g & g in dom f ) )
assume A4: x0 < r ; :: thesis: ex g being Real st
( g < r & x0 < g & g in dom f )
x0 - 1 < x0 by Lm1;
then consider g1, g2 being Real such that
A5: ( x0 - 1 < g1 & g1 < x0 & g1 in dom f & g2 < r & x0 < g2 & g2 in dom f ) by A1, A4;
take g2 ; :: thesis: ( g2 < r & x0 < g2 & g2 in dom f )
thus ( g2 < r & x0 < g2 & g2 in dom f ) by A5; :: thesis: verum

end;

assume A6: ( ( 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: 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 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 A7: ( 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
A8: ( r1 < g1 & g1 < x0 & g1 in dom f ) by A6;
consider g2 being Real such that
A9: ( g2 < r2 & x0 < g2 & g2 in dom f ) by A6, A7;
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 A8, A9; :: thesis: verum