let G be _Graph; :: thesis: for V, E being set
for G1, G2 being inducedSubgraph of G,V,E holds G1 == G2
let V, E be set ; :: thesis: for G1, G2 being inducedSubgraph of G,V,E holds G1 == G2
let G1, G2 be inducedSubgraph of G,V,E; :: thesis: G1 == G2

now

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

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

then ( the_Vertices_of G1 = V & the_Vertices_of G2 = V & the_Edges_of G1 = E & the_Edges_of G2 = E ) by Def39;
hence G1 == G2 by Th89; :: thesis: verum

end;

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

then ( G1 == G & G2 == G ) by Def39;
hence G1 == G2 by Th88; :: thesis: verum

end;

end;

end;

hence G1 == G2 ; :: thesis: verum