let A be Subset of R^1; :: thesis: for a, b, c, d being Real 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; :: thesis: ( a < b & b < c & A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} implies Cl A = ].-infty,c.] \/ {d} )
assume that
A1: a < b and
A2: b < c and
A3: 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:17;
Cl A = (Cl (((B \/ C) \/ D) \/ E)) \/ (Cl F) by A3, PRE_TOPC:20
.= (Cl (((B \/ C) \/ D) \/ E)) \/ {d} by Th37 ;
hence Cl A = ].-infty,c.] \/ {d} by A1, A2, Th65; :: thesis: verum