let A be Subset of I[01] ; :: thesis: for a, b being real number st a < b & A = [.a,b.[ holds
Cl A = [.a,b.]
let a, b be real number ; :: thesis: ( a < b & A = [.a,b.[ implies Cl A = [.a,b.] )
assume A1: ( a < b & A = [.a,b.[ ) ; :: thesis: Cl A = [.a,b.]
then A2: Cl [.a,b.[ = [.a,b.] by Th21;
reconsider A1 = [.a,b.[ as Subset of R^1 by TOPMETR:24;
Cl A = (Cl A1) /\ ([#] I[01] ) by A1, PRE_TOPC:47
.= [.a,b.] /\ ([#] I[01] ) by A2, TOPREAL6:80
.= [.a,b.] by A1, Th19, XBOOLE_1:28 ;
hence Cl A = [.a,b.] ; :: thesis: verum