let A be Subset of R^1; :: thesis: for a being Real st A = ].a,+infty.[ holds
Cl A = [.a,+infty.[
let a be Real; :: 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 Th39;
C is closed by Th41;
then A3: Cl A9 c= C by A1, TOPS_1:5, XXREAL_1:45;
A4: C = A9 \/ {a} by A1, Th42;
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 = [.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, Th33, Th44; :: thesis: verum
end;
end;