for G being SimpleGraph holds Vertices G = Vertices (Complement G) by Lm4;