let A be Subset of I[01]; :: thesis: for a, b being Real st a < b & A = ].a,b.[ holds
Cl A = [.a,b.]
let a, b be Real; :: thesis: ( a < b & A = ].a,b.[ implies Cl A = [.a,b.] )
assume that
A1: a < b and
A2: A = ].a,b.[ ; :: thesis: Cl A = [.a,b.]
reconsider A1 = ].a,b.[ as Subset of R^1 by TOPMETR:17;
A3: Cl ].a,b.[ = [.a,b.] by A1, JORDAN5A:26;
Cl A = (Cl A1) /\ ([#] I[01]) by A2, PRE_TOPC:17
.= [.a,b.] /\ ([#] I[01]) by A3, JORDAN5A:24
.= [.a,b.] by A1, A2, Th5, XBOOLE_1:28 ;
hence Cl A = [.a,b.] ; :: thesis: verum