let A be Subset of R^1 ; :: thesis: 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 ; :: thesis: ( a < b & b < c & A = ((].-infty ,a.[ \/ ].a,b.]) \/ (IRRAT b,c)) \/ {c} implies Cl A = ].-infty ,c.] )
assume A1: ( a < b & b < c & 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:24;
A2: ( c in E & c in ].-infty ,c.] ) by TARSKI:def 1, XXREAL_1:234;
Cl A = (Cl ((B \/ C) \/ D)) \/ (Cl E) by A1, 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 A1, Th55
.= ].-infty ,c.] \/ E by A1, Th29
.= ].-infty ,c.] by A2, ZFMISC_1:46 ;
hence Cl A = ].-infty ,c.] ; :: thesis: verum