let GX be non empty TopSpace; :: thesis: for V being Subset of GX st V is connected & V <> {} holds

Component_of (Component_of V) = Component_of V

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

assume ( V is connected & V <> {} ) ; :: thesis: Component_of (Component_of V) = Component_of V

then Component_of V is a_component by Th8;

hence Component_of (Component_of V) = Component_of V by Th7; :: thesis: verum

Component_of (Component_of V) = Component_of V

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

assume ( V is connected & V <> {} ) ; :: thesis: Component_of (Component_of V) = Component_of V

then Component_of V is a_component by Th8;

hence Component_of (Component_of V) = Component_of V by Th7; :: thesis: verum