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 A9 = A as Subset of R^1 ;
reconsider C = [.a,+infty.[ as Subset of R^1 by TOPMETR:17;
assume A1: A = ].a,+infty.[ ; :: thesis: Cl A = [.a,+infty.[
then A2: A9 is open by Th63;
C is closed by Th66;
then A3: Cl A9 c= C by A1, TOPS_1:5, XXREAL_1:45;
A4: C = A9 \/ {a} by A1, Th67;

per cases ( Cl A9 = C or Cl A9 = A9 ) by A4, A3, Th2, PRE_TOPC:18;

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

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

end;

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

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

end;

end;