let G1, G2 be _Graph; for G3 being SimpleGraph of G1 st G1 == G2 holds
G3 is SimpleGraph of G2
let G3 be SimpleGraph of G1; ( G1 == G2 implies G3 is SimpleGraph of G2 )
consider E being RepEdgeSelection of G1 such that
A1:
G3 is inducedSubgraph of G1, the_Vertices_of G1,E \ (G1 .loops())
by Def9;
assume A2:
G1 == G2
; G3 is SimpleGraph of G2
then A3:
( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )
by GLIB_000:def 34;
then A4:
G3 is inducedSubgraph of G2, the_Vertices_of G2,E \ (G1 .loops())
by A1, A2, GLIB_000:95;
A5:
G1 .loops() = G2 .loops()
by A2, Th50;
G2 is Subgraph of G1
by A2, GLIB_000:87;
then
E is RepEdgeSelection of G2
by A3, Th78;
hence
G3 is SimpleGraph of G2
by A4, A5, Def9; verum