theorem :: SCMYCIEL:40

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