let G2 be _Graph; :: thesis: for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 holds G2 is inducedSubgraph of G1,(the_Vertices_of G2)
let v1, e, v2 be object ; :: thesis: for G1 being addAdjVertex of G2,v1,e,v2 holds G2 is inducedSubgraph of G1,(the_Vertices_of G2)
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis: G2 is inducedSubgraph of G1,(the_Vertices_of G2)

per cases ( ( v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) or ( not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) or ( ( not v1 in the_Vertices_of G2 or v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) & ( v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ) ) ;

suppose ( v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: G2 is inducedSubgraph of G1,(the_Vertices_of G2)

then the_Vertices_of G1 = (the_Vertices_of G2) \/ {v2} by Def12;
then A1: the_Vertices_of G2 is non empty Subset of (the_Vertices_of G1) by XBOOLE_1:7;
A2: G2 is Subgraph of G1 by Th61;
the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G2) by Th139;
hence G2 is inducedSubgraph of G1,(the_Vertices_of G2) by A1, A2, GLIB_000:def 37; :: thesis: verum

end;

suppose ( not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: G2 is inducedSubgraph of G1,(the_Vertices_of G2)

then the_Vertices_of G1 = (the_Vertices_of G2) \/ {v1} by Def12;
then A3: the_Vertices_of G2 is non empty Subset of (the_Vertices_of G1) by XBOOLE_1:7;
A4: G2 is Subgraph of G1 by Th61;
the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G2) by Th139;
hence G2 is inducedSubgraph of G1,(the_Vertices_of G2) by A3, A4, GLIB_000:def 37; :: thesis: verum

end;

suppose ( ( not v1 in the_Vertices_of G2 or v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) & ( v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ) ; :: thesis: G2 is inducedSubgraph of G1,(the_Vertices_of G2)

then A5: G1 == G2 by Def12;
then A6: the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:def 34;
G1 is inducedSubgraph of G1,(the_Vertices_of G1) by GLIB_000:100;
hence G2 is inducedSubgraph of G1,(the_Vertices_of G2) by A5, A6, GLIB_000:101; :: thesis: verum

end;

end;