let G be _Graph; :: thesis: for E, V being set
for G1, G2 being inducedSubgraph of G,V,E holds G1 == G2
let E, V 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 :: thesis: G1 == G2

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 A1: ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; :: thesis: G1 == G2

then A2: ( the_Edges_of G1 = E & the_Edges_of G2 = E ) by Def37;
( the_Vertices_of G1 = V & the_Vertices_of G2 = V ) by A1, Def37;
hence G1 == G2 by A2, Th86; :: 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 Def37;
hence G1 == G2 ; :: thesis: verum

end;

end;

end;

hence G1 == G2 ; :: thesis: verum