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

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