let GX be TopSpace; :: thesis: for A being Subset of GX st A is connected holds
Cl A is connected
let A be Subset of GX; :: thesis: ( A is connected implies Cl A is connected )
A1: A c= Cl A by PRE_TOPC:18;
assume A is connected ; :: thesis: Cl A is connected
hence Cl A is connected by A1, Th18; :: thesis: verum