theorem :: SCMYCIEL:41

for G being SimpleGraph
for x, y being set st x <> y & x in Vertices G & y in Vertices G holds
( {x,y} in Edges G iff {x,y} nin Edges (Complement G) ) by Lm5;