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, JORDAN5A:26;
hence Cl A = [.a,b.] by A1, JORDAN5A:24; :: thesis: verum