let G2 be _Graph; :: thesis:
let v1, e, v2 be object ; :: thesis:
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis:

per cases ;

suppose ( v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis:

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:

end;

suppose ( not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis:

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:

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:

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 Th19;
hence G2 is inducedSubgraph of G1,(the_Vertices_of G2) by A5, A6, Th20; :: thesis:

end;

end;