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 A1: ( A = ].a,b.[ & a <> b ) ; :: thesis: Cl A = [.a,b.]
then Cl ].a,b.[ = [.a,b.] by TOPREAL6:82;
hence Cl A = [.a,b.] by A1, TOPREAL6:80; :: thesis: verum