let GX be non empty TopSpace; :: thesis: for V being Subset of GX st V is connected holds

Component_of V <> {}

let V be Subset of GX; :: thesis: ( V is connected implies Component_of V <> {} )

assume A1: V is connected ; :: thesis: Component_of V <> {}

Component_of V <> {}

let V be Subset of GX; :: thesis: ( V is connected implies Component_of V <> {} )

assume A1: V is connected ; :: thesis: Component_of V <> {}