let A be Subset of R^1; :: thesis: for a, b being real number st A = ].a,b.[ & a <> b holds
Cl A = [.a,b.]
let a, b be real number ; :: thesis: ( A = ].a,b.[ & a <> b implies Cl A = [.a,b.] )
assume that
A1: A = ].a,b.[ and
A2: a <> b ; :: thesis: Cl A = [.a,b.]
Cl ].a,b.[ = [.a,b.] by A2, TOPREAL6:73;
hence Cl A = [.a,b.] by A1, TOPREAL6:71; :: thesis: verum