theorem :: GLIB_009:44
for G1, G2 being plain _Graph st G1 == G2 holds
G1 = G2