let A be Subset of R^1 ; :: thesis: for a being real number st A = ].a,+infty .[ holds
Cl A = [.a,+infty .[
let a be real number ; :: thesis: ( A = ].a,+infty .[ implies Cl A = [.a,+infty .[ )
reconsider A' = A as Subset of R^1 ;
assume A1: A = ].a,+infty .[ ; :: thesis: Cl A = [.a,+infty .[
then A2: A' is open by Th63;
reconsider C = [.a,+infty .[ as Subset of R^1 by TOPMETR:24;
A3: C is closed by Th66;
A4: C = A' \/ {a} by A1, Th67;
A5: Cl A' c= C by A1, A3, TOPS_1:31, XXREAL_1:45;

per cases ( Cl A' = C or Cl A' = A' ) by A4, A5, Th2, PRE_TOPC:48;

suppose Cl A' = C ; :: thesis: Cl A = [.a,+infty .[

hence Cl A = [.a,+infty .[ ; :: thesis: verum

end;

suppose Cl A' = A' ; :: thesis: Cl A = [.a,+infty .[

hence Cl A = [.a,+infty .[ by A1, A2, Th57, Th71; :: thesis: verum

end;

end;