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