let A be Subset of R^1 ; :: thesis: for a, b being real number st a < b & A = ].a,b.[ \/ ].b,+infty .[ holds
Cl A = [.a,+infty .[
let a, b be real number ; :: thesis: ( a < b & A = ].a,b.[ \/ ].b,+infty .[ implies Cl A = [.a,+infty .[ )
assume A1: ( a < b & A = ].a,b.[ \/ ].b,+infty .[ ) ; :: thesis: Cl A = [.a,+infty .[
reconsider B = ].a,b.[, C = ].b,+infty .[ as Subset of R^1 by TOPMETR:24;
A2: Cl A = (Cl B) \/ (Cl C) by A1, PRE_TOPC:50;
A3: Cl B = [.a,b.] by A1, Th36;
Cl C = [.b,+infty .[ by Th75;
hence Cl A = [.a,+infty .[ by A1, A2, A3, Th28; :: thesis: verum