now :: thesis: for x being object st x in { the plain inducedSubgraph of G,V,E where V is non empty Subset of (the_Vertices_of G), E is Subset of (the_Edges_of G) : E c= G .edgesBetween V } holds
x is _Graph

let x be object ; :: thesis: ( x in { the plain inducedSubgraph of G,V,E where V is non empty Subset of (the_Vertices_of G), E is Subset of (the_Edges_of G) : E c= G .edgesBetween V } implies x is _Graph )
assume x in { the plain inducedSubgraph of G,V,E where V is non empty Subset of (the_Vertices_of G), E is Subset of (the_Edges_of G) : E c= G .edgesBetween V } ; :: thesis: x is _Graph
then consider V being non empty Subset of (the_Vertices_of G), E being Subset of (the_Edges_of G) such that
A1: x = the plain inducedSubgraph of G,V,E and
E c= G .edgesBetween V ;
thus x is _Graph by A1; :: thesis: verum

end;

hence { the plain inducedSubgraph of G,V,E where V is non empty Subset of (the_Vertices_of G), E is Subset of (the_Edges_of G) : E c= G .edgesBetween V } is Graph-membered set by GLIB_014:def 1; :: thesis: verum