theorem Th115: :: GLIB_012:115

for G1 being _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & G1 .order() = 2 holds
( ( v1 is endvertex implies v2 is isolated ) & ( v1 is isolated implies v2 is endvertex ) )