let a, b be Real; :: thesis: for Z being open Subset of REAL st a < b & [.a,b.] c= Z holds
ex a1, b1 being Real st
( a1 < a & b < b1 & a1 < b1 & [.a1,b1.] c= Z & [.a,b.] c= ].a1,b1.[ )
let Z be open Subset of REAL; :: thesis: ( a < b & [.a,b.] c= Z implies ex a1, b1 being Real st
( a1 < a & b < b1 & a1 < b1 & [.a1,b1.] c= Z & [.a,b.] c= ].a1,b1.[ ) )
assume A1: ( a < b & [.a,b.] c= Z ) ; :: thesis: ex a1, b1 being Real st
( a1 < a & b < b1 & a1 < b1 & [.a1,b1.] c= Z & [.a,b.] c= ].a1,b1.[ )
then a in [.a,b.] ;
then consider d1 being Real such that
A2: ( 0 < d1 & ].(a - d1),(a + d1).[ c= Z ) by A1, RCOMP_1:19;
b in [.a,b.] by A1;
then consider d2 being Real such that
A3: ( 0 < d2 & ].(b - d2),(b + d2).[ c= Z ) by A1, RCOMP_1:19;
reconsider d = min (d1,d2) as Real ;
A4: ( d <= d1 & d <= d2 ) by XXREAL_0:17;
A5: 0 < d by A2, A3, XXREAL_0:15;
then A6: ( 0 < d / 2 & d / 2 < d ) by XREAL_1:216;
set a1 = a - (d / 2);
set b1 = b + (d / 2);
take a - (d / 2) ; :: thesis: ex b1 being Real st
( a - (d / 2) < a & b < b1 & a - (d / 2) < b1 & [.(a - (d / 2)),b1.] c= Z & [.a,b.] c= ].(a - (d / 2)),b1.[ )
take b + (d / 2) ; :: thesis: ( a - (d / 2) < a & b < b + (d / 2) & a - (d / 2) < b + (d / 2) & [.(a - (d / 2)),(b + (d / 2)).] c= Z & [.a,b.] c= ].(a - (d / 2)),(b + (d / 2)).[ )
A7: a - (d / 2) < a - 0 by A5, XREAL_1:15;
then A8: a - (d / 2) < b by A1, XXREAL_0:2;
A9: b + 0 < b + (d / 2) by A5, XREAL_1:8;
hence ( a - (d / 2) < a & b < b + (d / 2) & a - (d / 2) < b + (d / 2) ) by A7, A8, XXREAL_0:2; :: thesis: ( [.(a - (d / 2)),(b + (d / 2)).] c= Z & [.a,b.] c= ].(a - (d / 2)),(b + (d / 2)).[ )
thus [.(a - (d / 2)),(b + (d / 2)).] c= Z :: thesis: [.a,b.] c= ].(a - (d / 2)),(b + (d / 2)).[

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in [.(a - (d / 2)),(b + (d / 2)).] or t in Z )
assume A11: t in [.(a - (d / 2)),(b + (d / 2)).] ; :: thesis: t in Z
then reconsider s = t as Real ;

per cases ( ( a - (d / 2) <= s & s < a ) or ( a <= s & s <= b ) or ( b < s & s <= b + (d / 2) ) ) by A11, XXREAL_1:1;

suppose A13: ( a - (d / 2) <= s & s < a ) ; :: thesis: t in Z

A14: a - d < a - (d / 2) by A6, XREAL_1:15;
a - d1 <= a - d by A4, XREAL_1:13;
then a - d1 < a - (d / 2) by A14, XXREAL_0:2;
then A15: a - d1 < s by A13, XXREAL_0:2;
a + 0 < a + d1 by A2, XREAL_1:8;
then s < a + d1 by A13, XXREAL_0:2;
then t in ].(a - d1),(a + d1).[ by A15;
hence t in Z by A2; :: thesis: verum

end;

suppose ( a <= s & s <= b ) ; :: thesis: t in Z

then t in [.a,b.] ;
hence t in Z by A1; :: thesis: verum

end;

suppose A16: ( b < s & s <= b + (d / 2) ) ; :: thesis: t in Z

A17: b + (d / 2) < b + d by A6, XREAL_1:8;
b + d <= b + d2 by A4, XREAL_1:7;
then b + (d / 2) < b + d2 by A17, XXREAL_0:2;
then A18: s < b + d2 by A16, XXREAL_0:2;
b - d2 < b - 0 by A3, XREAL_1:15;
then b - d2 < s by A16, XXREAL_0:2;
then t in ].(b - d2),(b + d2).[ by A18;
hence t in Z by A3; :: thesis: verum

end;

end;

end;

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in [.a,b.] or t in ].(a - (d / 2)),(b + (d / 2)).[ )
assume A20: t in [.a,b.] ; :: thesis: t in ].(a - (d / 2)),(b + (d / 2)).[
then reconsider s = t as Real ;
( a <= s & s <= b ) by A20, XXREAL_1:1;
then ( a - (d / 2) < s & s < b + (d / 2) ) by A7, A9, XXREAL_0:2;
hence t in ].(a - (d / 2)),(b + (d / 2)).[ ; :: thesis: verum