for S being non empty Graph-membered connected set holds { (H .componentSet()) where H is Element of S : verum } = SmallestPartition (the_Vertices_of S)