let A be Subset of R^1 ; :: thesis: for a, b, c, d being real number st a < b & b < c & A = (((].-infty ,a.[ \/ ].a,b.]) \/ (IRRAT b,c)) \/ {c}) \/ {d} holds
Cl A = ].-infty ,c.] \/ {d}
let a, b, c, d be real number ; :: thesis: ( a < b & b < c & A = (((].-infty ,a.[ \/ ].a,b.]) \/ (IRRAT b,c)) \/ {c}) \/ {d} implies Cl A = ].-infty ,c.] \/ {d} )
assume A1: ( a < b & b < c & A = (((].-infty ,a.[ \/ ].a,b.]) \/ (IRRAT b,c)) \/ {c}) \/ {d} ) ; :: thesis: Cl A = ].-infty ,c.] \/ {d}
reconsider B = ].-infty ,a.[, C = ].a,b.], D = IRRAT b,c, E = {c}, F = {d} as Subset of R^1 by TOPMETR:24;
Cl A = (Cl (((B \/ C) \/ D) \/ E)) \/ (Cl F) by A1, PRE_TOPC:50
.= (Cl (((B \/ C) \/ D) \/ E)) \/ {d} by Th61 ;
hence Cl A = ].-infty ,c.] \/ {d} by A1, Th100; :: thesis: verum