theorem :: GLIB_000:85

for G1, G2, G3 being _Graph st G1 == G2 & G2 == G3 holds
G1 == G3 ;