let G3 be _Graph; :: thesis: for G2 being Supergraph of G3
for G1 being Supergraph of G2 holds G1 is Supergraph of G3
let G2 be Supergraph of G3; :: thesis: for G1 being Supergraph of G2 holds G1 is Supergraph of G3
let G1 be Supergraph of G2; :: thesis: G1 is Supergraph of G3
( G3 is Subgraph of G2 & G2 is Subgraph of G1 ) by Th61;
then G3 is Subgraph of G1 by GLIB_000:43;
hence G1 is Supergraph of G3 by Th61; :: thesis: verum