theorem Th20: :: GLIB_013:20

for G1, G2 being _Graph
for c being Cardinal st G1 == G2 holds
( ( G1 is c -vertex implies G2 is c -vertex ) & ( G1 is c -edge implies G2 is c -edge ) ) by GLIB_000:def 34;