let A be Subset of R^1; for a, b, c being Real st A = [.a,b.[ \/ ].b,c.] & a < b & b < c holds
Cl A = [.a,c.]
let a, b, c be Real; ( A = [.a,b.[ \/ ].b,c.] & a < b & b < c implies Cl A = [.a,c.] )
assume that
A1:
A = [.a,b.[ \/ ].b,c.]
and
A2:
a < b
and
A3:
b < c
; Cl A = [.a,c.]
reconsider B = [.a,b.[, C = ].b,c.] as Subset of R^1 by TOPMETR:17;
Cl A =
(Cl B) \/ (Cl C)
by A1, PRE_TOPC:20
.=
[.a,b.] \/ (Cl C)
by A2, Th34
.=
[.a,b.] \/ [.b,c.]
by A3, Th35
.=
[.a,c.]
by A2, A3, XXREAL_1:174
;
hence
Cl A = [.a,c.]
; verum