let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V holds G2 is inducedSubgraph of G1,(the_Vertices_of G2)
let V be set ; :: thesis: for G1 being addVertices of G2,V holds G2 is inducedSubgraph of G1,(the_Vertices_of G2)
let G1 be addVertices of G2,V; :: thesis: G2 is inducedSubgraph of G1,(the_Vertices_of G2)
set V2 = the_Vertices_of G2;
reconsider G3 = G2 as Subgraph of G1 by Th61;
A2: the_Vertices_of G3 = the_Vertices_of G2 ;
A3: the_Edges_of G3 = the_Edges_of G1 by Def10
.= G1 .edgesBetween (the_Vertices_of G2) by Th85 ;
thus G2 is inducedSubgraph of G1,(the_Vertices_of G2) by A2, A3, GLIB_000:def 37; :: thesis: verum