let A be Subset of R^1; for a, b, c being Real st A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c holds
Int A = ].-infty,a.[
let a, b, c be Real; ( A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c implies Int A = ].-infty,a.[ )
reconsider B = [.a,b.], C = IRRAT (b,c), D = [.c,+infty.[ as Subset of R^1 by TOPMETR:17;
assume that
A1:
A = ].-infty,a.[ \/ (RAT (b,c))
and
A2:
a < b
and
A3:
b < c
; Int A = ].-infty,a.[
A4:
a < c
by A2, A3, XXREAL_0:2;
A ` =
REAL \ (].-infty,a.[ \/ (RAT (b,c)))
by A1, TOPMETR:17
.=
(REAL \ (RAT (b,c))) \ ].-infty,a.[
by XBOOLE_1:41
.=
((].-infty,b.] \/ (IRRAT (b,c))) \/ [.c,+infty.[) \ ].-infty,a.[
by BORSUK_5:58
.=
(].-infty,b.] \/ ((IRRAT (b,c)) \/ [.c,+infty.[)) \ ].-infty,a.[
by XBOOLE_1:4
.=
(].-infty,b.] \ ].-infty,a.[) \/ (((IRRAT (b,c)) \/ [.c,+infty.[) \ ].-infty,a.[)
by XBOOLE_1:42
;
then A5: A ` =
[.a,b.] \/ (((IRRAT (b,c)) \/ [.c,+infty.[) \ ].-infty,a.[)
by XXREAL_1:289
.=
[.a,b.] \/ (((IRRAT (b,c)) \ ].-infty,a.[) \/ ([.c,+infty.[ \ ].-infty,a.[))
by XBOOLE_1:42
;
right_closed_halfline c is closed
;
then
D is closed
by JORDAN5A:23;
then A6:
Cl D = D
by PRE_TOPC:22;
[.b,+infty.[ misses ].-infty,a.[
by A2, XXREAL_1:94;
then
IRRAT (b,c) misses ].-infty,a.[
by Th31, XBOOLE_1:63;
then A7:
(IRRAT (b,c)) \ ].-infty,a.[ = IRRAT (b,c)
by XBOOLE_1:83;
B is closed
by JORDAN5A:23;
then A8:
Cl B = B
by PRE_TOPC:22;
[.c,+infty.[ misses ].-infty,a.[
by A2, A3, XXREAL_0:2, XXREAL_1:94;
then A ` =
[.a,b.] \/ ((IRRAT (b,c)) \/ [.c,+infty.[)
by A5, A7, XBOOLE_1:83
.=
[.a,b.] \/ ((IRRAT (b,c)) \/ ({c} \/ ].c,+infty.[))
by BORSUK_5:43
.=
([.a,b.] \/ (IRRAT (b,c))) \/ ({c} \/ ].c,+infty.[)
by XBOOLE_1:4
.=
([.a,b.] \/ (IRRAT (b,c))) \/ [.c,+infty.[
by BORSUK_5:43
;
then Cl (A `) =
(Cl (B \/ C)) \/ (Cl D)
by PRE_TOPC:20
.=
((Cl B) \/ (Cl C)) \/ (Cl D)
by PRE_TOPC:20
.=
(B \/ [.b,c.]) \/ D
by A8, A6, A3, BORSUK_5:32
.=
[.a,c.] \/ D
by A2, A3, XXREAL_1:165
.=
[.a,+infty.[
by A4, BORSUK_5:11
;
then
(Cl (A `)) ` = ].-infty,a.[
by TOPMETR:17, XXREAL_1:224, XXREAL_1:294;
hence
Int A = ].-infty,a.[
by TOPS_1:def 1; verum