let A be Subset of R^1; :: thesis: for a, b, c being Real 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; :: thesis: ( 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} ; :: thesis: Cl A = ].-infty,c.]
reconsider B = ].-infty,a.[, C = ].a,b.], D = IRRAT (b,c), E = {c} as Subset of R^1 by TOPMETR:17;
A4: c in ].-infty,c.] by XXREAL_1:234;
Cl A = (Cl ((B \/ C) \/ D)) \/ (Cl E) by A3, PRE_TOPC:20
.= (Cl ((B \/ C) \/ D)) \/ E by Th37
.= ((Cl (B \/ C)) \/ (Cl D)) \/ E by PRE_TOPC:20
.= (].-infty,b.] \/ (Cl D)) \/ E by A1, Th64
.= (].-infty,b.] \/ [.b,c.]) \/ E by A2, Th31
.= ].-infty,c.] \/ E by A2, Th11
.= ].-infty,c.] by A4, ZFMISC_1:40 ;
hence Cl A = ].-infty,c.] ; :: thesis: verum