let G1, G2, G3 be _Graph; :: thesis: ( G1 == G2 & G2 == G3 implies G1 == G3 )
assume that
A1: G1 == G2 and
A2: G2 == G3 ; :: thesis: G1 == G3
A3: ( the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) by A1, Def36;
A4: ( the_Source_of G2 = the_Source_of G3 & the_Target_of G2 = the_Target_of G3 ) by A2, Def36;
A5: ( the_Vertices_of G2 = the_Vertices_of G3 & the_Edges_of G2 = the_Edges_of G3 ) by A2, Def36;
( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by A1, Def36;
hence G1 == G3 by A3, A5, A4, Def36; :: thesis: verum