let A be Subset of R^1; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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.] ; :: thesis: verum