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

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 A3: ( V is non empty Subset of (the_Vertices_of G1) & E c= G1 .edgesBetween V ) ; :: thesis: G3 is inducedSubgraph of G1,V,E

then ( the_Vertices_of G2 = V & the_Edges_of G2 = E ) by Def37;
then ( the_Vertices_of G3 = V & the_Edges_of G3 = E ) by A1;
hence G3 is inducedSubgraph of G1,V,E by A2, A3, Def37; :: thesis: verum

end;

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

then G2 == G1 by Def37;
then G3 == G1 by A1;
hence G3 is inducedSubgraph of G1,V,E by A2, A4, Def37; :: thesis: verum

end;

end;