let a, b be real number ; :: 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.]
reconsider a1 =
a,
b1 =
b as
Real by XREAL_0:def 1;
per cases
( a > b or a < b )
by A1, XXREAL_0:1;
suppose A3:
a < b
;
:: thesis: Cl ].a,b.[ = [.a,b.]
].a,b.[ c= [.a,b.]
by XXREAL_1:25;
hence
Cl ].a,b.[ c= [.a,b.]
by PSCOMP_1:32;
:: according to XBOOLE_0:def 10 :: thesis: [.a,b.] c= Cl ].a,b.[A4:
[.a,b.] = { w where w is Real : ( a <= w & w <= b ) }
by RCOMP_1:def 1;
A5:
].a,b.[ = { w where w is Real : ( a < w & w < b ) }
by RCOMP_1:def 2;
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in [.a,b.] or p in Cl ].a,b.[ )assume
p in [.a,b.]
;
:: thesis: p in Cl ].a,b.[then consider r being
Real such that A6:
p = r
and A7:
(
a <= r &
r <= b )
by A4;
(
a1 < (a1 + b1) / 2 &
(a1 + b1) / 2
< b1 )
by A3, XREAL_1:228;
then A8:
(a1 + b1) / 2
in ].a1,b1.[
by A5;
now per cases
( ( a < r & r < b ) or a = r or b = r )
by A7, XXREAL_0:1;
case A10:
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 number such that A11:
0 < g
and A12:
].(a - g),(a + g).[ c= O
by RCOMP_1:40;
reconsider g =
g as
Real by XREAL_0:def 1;
A13:
].(a - g),(a + g).[ = { w where w is Real : ( a - g < w & w < a + g ) }
by RCOMP_1:def 2;
A14:
a - g < a - 0
by A11, XREAL_1:17;
per cases
( a + g < b or a + g >= b )
;
suppose A15:
a + g < b
;
:: thesis: not O /\ ].a,b.[ is empty A16:
a + 0 < a + g
by A11, XREAL_1:8;
then A17:
a1 < (a1 + (a1 + g)) / 2
by XREAL_1:228;
then A18:
a - g < (a + (a + g)) / 2
by A14, XXREAL_0:2;
A19:
(a1 + (a1 + g)) / 2
< a1 + g
by A16, XREAL_1:228;
then A20:
(a1 + (a1 + g)) / 2
in ].(a1 - g),(a1 + g).[
by A13, A18;
(a + (a + g)) / 2
< b
by A15, A19, XXREAL_0:2;
then
(a1 + (a1 + g)) / 2
in ].a1,b1.[
by A5, A17;
hence
not
O /\ ].a,b.[ is
empty
by A12, A20, XBOOLE_0:def 4;
:: thesis: verum end;
end; hence
p in Cl ].a,b.[
by A6, A10, PSCOMP_1:38;
:: thesis: verum case A23:
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 number such that A24:
0 < g
and A25:
].(b - g),(b + g).[ c= O
by RCOMP_1:40;
reconsider g =
g as
Real by XREAL_0:def 1;
A26:
].(b - g),(b + g).[ = { w where w is Real : ( b - g < w & w < b + g ) }
by RCOMP_1:def 2;
A27:
b - g < b - 0
by A24, XREAL_1:17;
A28:
b + 0 < b + g
by A24, XREAL_1:8;
per cases
( b - g > a or b - g <= a )
;
suppose A29:
b - g > a
;
:: thesis: not O /\ ].a,b.[ is empty A30:
b1 - g < (b1 + (b1 - g)) / 2
by A27, XREAL_1:228;
then A31:
a < (b + (b - g)) / 2
by A29, XXREAL_0:2;
(b1 + (b1 - g)) / 2
< b1
by A27, XREAL_1:228;
then
(b + (b - g)) / 2
< b + g
by A28, XXREAL_0:2;
then A32:
(b1 + (b1 - g)) / 2
in ].(b1 - g),(b1 + g).[
by A26, A30;
(b1 + (b1 - g)) / 2
< b1
by A27, XREAL_1:228;
then
(b1 + (b1 - g)) / 2
in ].a1,b1.[
by A5, A31;
hence
not
O /\ ].a,b.[ is
empty
by A25, A32, XBOOLE_0:def 4;
:: thesis: verum end;
end; hence
p in Cl ].a,b.[
by A6, A23, PSCOMP_1:38;
:: thesis: verum hence
p in Cl ].a,b.[
;
:: thesis: verum end;
end;
assume that
A35:
Cl ].a,b.[ = [.a,b.]
and
A36:
a = b
; :: thesis: contradiction
[.a,b.] = {a}
by A36, XXREAL_1:17;
hence
contradiction
by A35, A36, PSCOMP_1:35, XXREAL_1:28; :: thesis: verum