let A be Subset of R^1; for a being Real st A = ].-infty,a.[ holds
Cl A = ].-infty,a.]
let a be Real; ( 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.[
; 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;