let a, b be Real; :: thesis: ( a <> b iff Cl ].a,b.[ = [.a,b.] )
thus ( a <> b implies Cl ].a,b.[ = [.a,b.] ) :: thesis: ( Cl ].a,b.[ = [.a,b.] implies a <> b )
proof
assume A1: a <> b ; :: thesis: Cl ].a,b.[ = [.a,b.]
per cases ( a > b or a < b ) by A1, XXREAL_0:1;
suppose A3: a < b ; :: thesis: Cl ].a,b.[ = [.a,b.]
then A4: (a + b) / 2 < b by XREAL_1:226;
thus Cl ].a,b.[ c= [.a,b.] by MEASURE6:57, XXREAL_1:25; :: according to XBOOLE_0:def 10 :: thesis: [.a,b.] c= Cl ].a,b.[
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in [.a,b.] or p in Cl ].a,b.[ )
A5: ].a,b.[ = { w where w is Real : ( a < w & w < b ) } by RCOMP_1:def 2;
assume A6: p in [.a,b.] ; :: thesis: p in Cl ].a,b.[
[.a,b.] = { w where w is Real : ( a <= w & w <= b ) } by RCOMP_1:def 1;
then consider r being Real such that
A7: p = r and
A8: a <= r and
A9: r <= b by A6;
a < (a + b) / 2 by A3, XREAL_1:226;
then A10: (a + b) / 2 in ].a,b.[ by A5, A4;
now :: thesis: ( ( a < r & r < b & p in Cl ].a,b.[ ) or ( a = r & p in Cl ].a,b.[ ) or ( b = r & p in Cl ].a,b.[ ) )
per cases ( ( a < r & r < b ) or a = r or b = r ) by A8, A9, XXREAL_0:1;
case A11: ( a < r & r < b ) ; :: thesis: p in Cl ].a,b.[
A12: ].a,b.[ c= Cl ].a,b.[ by MEASURE6:58;
r in ].a,b.[ by A5, A11;
hence p in Cl ].a,b.[ by A7, A12; :: thesis: verum
end;
case A13: a = r ; :: thesis: p in Cl ].a,b.[
for O being open Subset of REAL st a in O holds
not O /\ ].a,b.[ is empty
proof
let O be open Subset of REAL; :: thesis: ( a in O implies not O /\ ].a,b.[ is empty )
assume a in O ; :: thesis: not O /\ ].a,b.[ is empty
then consider g being Real such that
A14: 0 < g and
A15: ].(a - g),(a + g).[ c= O by RCOMP_1:19;
A16: a - g < a - 0 by A14, XREAL_1:15;
A17: ].(a - g),(a + g).[ = { w where w is Real : ( a - g < w & w < a + g ) } by RCOMP_1:def 2;
per cases ( a + g < b or a + g >= b ) ;
suppose A18: a + g < b ; :: thesis: not O /\ ].a,b.[ is empty
A19: a + 0 < a + g by A14, XREAL_1:6;
then A20: a < (a + (a + g)) / 2 by XREAL_1:226;
A21: (a + (a + g)) / 2 < a + g by A19, XREAL_1:226;
then (a + (a + g)) / 2 < b by A18, XXREAL_0:2;
then A22: (a + (a + g)) / 2 in ].a,b.[ by A5, A20;
a - g < (a + (a + g)) / 2 by A16, A20, XXREAL_0:2;
then (a + (a + g)) / 2 in ].(a - g),(a + g).[ by A17, A21;
hence not O /\ ].a,b.[ is empty by A15, A22, XBOOLE_0:def 4; :: thesis: verum
end;
suppose A23: a + g >= b ; :: thesis: not O /\ ].a,b.[ is empty
(a + b) / 2 < b by A3, XREAL_1:226;
then A24: (a + b) / 2 < a + g by A23, XXREAL_0:2;
a < (a + b) / 2 by A3, XREAL_1:226;
then a - g < (a + b) / 2 by A16, XXREAL_0:2;
then (a + b) / 2 in ].(a - g),(a + g).[ by A17, A24;
hence not O /\ ].a,b.[ is empty by A10, A15, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence p in Cl ].a,b.[ by A7, A13, MEASURE6:63; :: thesis: verum
end;
case A25: b = r ; :: thesis: p in Cl ].a,b.[
for O being open Subset of REAL st b in O holds
not O /\ ].a,b.[ is empty
proof
let O be open Subset of REAL; :: thesis: ( b in O implies not O /\ ].a,b.[ is empty )
assume b in O ; :: thesis: not O /\ ].a,b.[ is empty
then consider g being Real such that
A26: 0 < g and
A27: ].(b - g),(b + g).[ c= O by RCOMP_1:19;
A28: b - g < b - 0 by A26, XREAL_1:15;
A29: b + 0 < b + g by A26, XREAL_1:6;
A30: ].(b - g),(b + g).[ = { w where w is Real : ( b - g < w & w < b + g ) } by RCOMP_1:def 2;
per cases ( b - g > a or b - g <= a ) ;
suppose A31: b - g > a ; :: thesis: not O /\ ].a,b.[ is empty
A32: (b + (b - g)) / 2 < b by A28, XREAL_1:226;
A33: b - g < (b + (b - g)) / 2 by A28, XREAL_1:226;
then a < (b + (b - g)) / 2 by A31, XXREAL_0:2;
then A34: (b + (b - g)) / 2 in ].a,b.[ by A5, A32;
(b + (b - g)) / 2 < b by A28, XREAL_1:226;
then (b + (b - g)) / 2 < b + g by A29, XXREAL_0:2;
then (b + (b - g)) / 2 in ].(b - g),(b + g).[ by A30, A33;
hence not O /\ ].a,b.[ is empty by A27, A34, XBOOLE_0:def 4; :: thesis: verum
end;
suppose A35: b - g <= a ; :: thesis: not O /\ ].a,b.[ is empty
(a + b) / 2 < b by A3, XREAL_1:226;
then A36: (a + b) / 2 < b + g by A29, XXREAL_0:2;
a < (a + b) / 2 by A3, XREAL_1:226;
then b - g < (a + b) / 2 by A35, XXREAL_0:2;
then (a + b) / 2 in ].(b - g),(b + g).[ by A30, A36;
hence not O /\ ].a,b.[ is empty by A10, A27, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence p in Cl ].a,b.[ by A7, A25, MEASURE6:63; :: thesis: verum
end;
end;
end;
hence p in Cl ].a,b.[ ; :: thesis: verum
end;
end;
end;
assume that
A37: Cl ].a,b.[ = [.a,b.] and
A38: a = b ; :: thesis: contradiction
[.a,b.] = {a} by A38, XXREAL_1:17;
hence contradiction by A37, A38, MEASURE6:60, XXREAL_1:28; :: thesis: verum