let A be Subset of R^1 ; for a, b, c being real number st a < b & b < c & A = ((].-infty ,a.[ \/ ].a,b.]) \/ (IRRAT b,c)) \/ {c} holds
Cl A = ].-infty ,c.]
let a, b, c be real number ; ( a < b & b < c & A = ((].-infty ,a.[ \/ ].a,b.]) \/ (IRRAT b,c)) \/ {c} implies Cl A = ].-infty ,c.] )
assume that
A1:
a < b
and
A2:
b < c
and
A3:
A = ((].-infty ,a.[ \/ ].a,b.]) \/ (IRRAT b,c)) \/ {c}
; Cl A = ].-infty ,c.]
reconsider B = ].-infty ,a.[, C = ].a,b.], D = IRRAT b,c, E = {c} as Subset of R^1 by TOPMETR:24;
A4:
c in ].-infty ,c.]
by XXREAL_1:234;
Cl A =
(Cl ((B \/ C) \/ D)) \/ (Cl E)
by A3, PRE_TOPC:50
.=
(Cl ((B \/ C) \/ D)) \/ E
by Th61
.=
((Cl (B \/ C)) \/ (Cl D)) \/ E
by PRE_TOPC:50
.=
(].-infty ,b.] \/ (Cl D)) \/ E
by A1, Th97
.=
(].-infty ,b.] \/ [.b,c.]) \/ E
by A2, Th55
.=
].-infty ,c.] \/ E
by A2, Th29
.=
].-infty ,c.]
by A4, ZFMISC_1:46
;
hence
Cl A = ].-infty ,c.]
; verum