let A be Subset of R^1; :: thesis: for a, b being Real st A = ].a,b.] & a <> b holds
Cl A = [.a,b.]
let a, b be Real; :: 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, BORSUK_4:11;
hence Cl A = [.a,b.] by A1, JORDAN5A:24; :: thesis: verum