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 :: thesis: G3 is inducedSubgraph of G2,V,E

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: ( the_Vertices_of G3 = V & the_Edges_of G3 = E ) by Def37;
A4: G3 is Subgraph of G2 by A1, Th91;
( V is non empty Subset of (the_Vertices_of G2) & E c= G2 .edgesBetween V ) by A1, A2, Th90;
hence G3 is inducedSubgraph of G2,V,E by A3, A4, Def37; :: 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, Th90;
G3 == G1 by A5, Def37;
then A7: G3 == G2 by A1;
then G3 is Subgraph of G2 by Th87;
hence G3 is inducedSubgraph of G2,V,E by A6, A7, Def37; :: thesis: verum

end;

end;

end;

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