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