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

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

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

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

end;

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

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

end;

end;