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 that
A1: a < b and
A2: 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;
A3: Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:50;
A4: Cl C = [.b,+infty .[ by Th75;
Cl B = [.a,b.] by A1, Th36;
hence Cl A = [.a,+infty .[ by A1, A3, A4, Th28; :: thesis: verum