let G1, G2 be _Graph; :: thesis: for V, E being set
for G3 being inducedSubgraph of G1,V,E st G1 == G2 holds
G3 is inducedSubgraph of G2,V,E
let V, E be set ; :: thesis: for G3 being inducedSubgraph of G1,V,E st G1 == G2 holds
G3 is inducedSubgraph of G2,V,E
let G3 be inducedSubgraph of G1,V,E; :: thesis: ( G1 == G2 implies G3 is inducedSubgraph of G2,V,E )
assume A1: G1 == G2 ; :: thesis: G3 is inducedSubgraph of G2,V,E

now

per cases ( ( V is non empty Subset of (the_Vertices_of G1) & E c= G1 .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G1) or not E c= G1 .edgesBetween V ) ;

suppose A2: ( V is non empty Subset of (the_Vertices_of G1) & E c= G1 .edgesBetween V ) ; :: thesis: G3 is inducedSubgraph of G2,V,E

then A3: ( V is non empty Subset of (the_Vertices_of G2) & E c= G2 .edgesBetween V ) by A1, Def36, Th93;
A4: ( the_Vertices_of G3 = V & the_Edges_of G3 = E ) by A2, Def39;
G3 is Subgraph of G2 by A1, Th94;
hence G3 is inducedSubgraph of G2,V,E by A3, A4, Def39; :: thesis: verum

end;

suppose A5: ( not V is non empty Subset of (the_Vertices_of G1) or not E c= G1 .edgesBetween V ) ; :: thesis: G3 is inducedSubgraph of G2,V,E

then A6: ( not V is non empty Subset of (the_Vertices_of G2) or not E c= G2 .edgesBetween V ) by A1, Def36, Th93;
G3 == G1 by A5, Def39;
then A7: G3 == G2 by A1, Th88;
then G3 is Subgraph of G2 by Th90;
hence G3 is inducedSubgraph of G2,V,E by A6, A7, Def39; :: thesis: verum

end;

end;

end;

hence G3 is inducedSubgraph of G2,V,E ; :: thesis: verum