let G1, G2 be _Graph; :: thesis: for G3 being removeLoops of G1 st G1 == G2 holds
G3 is removeLoops of G2
let G3 be removeLoops of G1; :: thesis: ( G1 == G2 implies G3 is removeLoops of G2 )
assume A1: G1 == G2 ; :: thesis: G3 is removeLoops of G2
then ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & G1 .loops() = G2 .loops() ) by Th50, GLIB_000:def 34;
hence G3 is removeLoops of G2 by A1, GLIB_000:95; :: thesis: verum