theorem Th147: :: GLIB_010:147

for G3 being _Graph
for G4 being b₁ -Disomorphic _Graph
for V1, V2 being set
for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2 st card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) holds
G2 is G1 -Disomorphic