take SmallestPartition (Vertices G) ; :: thesis: SmallestPartition (Vertices G) is StableSet-wise
thus SmallestPartition (Vertices G) is StableSet-wise by Coloring1; :: thesis: verum