let A be Subset of R^1; :: thesis: for a being Real st A = ].-infty,a.[ holds
Cl A = ].-infty,a.]
let a be Real; :: thesis: ( A = ].-infty,a.[ implies Cl A = ].-infty,a.] )
reconsider A9 = A as Subset of R^1 ;
reconsider C = ].-infty,a.] as Subset of R^1 by TOPMETR:17;
assume A1: A = ].-infty,a.[ ; :: thesis: Cl A = ].-infty,a.]
then A2: A9 is open by Th39;
C is closed by Th40;
then A3: Cl A9 c= C by A1, TOPS_1:5, XXREAL_1:41;
A4: C = A9 \/ {a} by A1, Th43;

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

suppose Cl A9 = C ; :: thesis: Cl A = ].-infty,a.]

hence Cl A = ].-infty,a.] ; :: thesis: verum

end;

suppose Cl A9 = A9 ; :: thesis: Cl A = ].-infty,a.]

hence Cl A = ].-infty,a.] by A1, A2, Th33, Th47; :: thesis: verum

end;

end;