let GX be non empty TopSpace; :: thesis: for A being Subset of GX st A is connected & A <> {} holds
Cl A c= Component_of A
let A be Subset of GX; :: thesis: ( A is connected & A <> {} implies Cl A c= Component_of A )
assume that
A1: A is connected and
A2: A <> {} ; :: thesis: Cl A c= Component_of A
Cl A is connected by A1, CONNSP_1:19;
hence Cl A c= Component_of A by A1, A2, Th13, PRE_TOPC:18; :: thesis: verum