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

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