theorem Th67: :: GLIB_015:67

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