let G be _Graph; :: thesis: for V being non empty Subset of (the_Vertices_of G)
for S, T being Function of {},V holds createGraph (V,{},S,T) in G .allSG()
let V be non empty Subset of (the_Vertices_of G); :: thesis: for S, T being Function of {},V holds createGraph (V,{},S,T) in G .allSG()
let S, T be Function of {},V; :: thesis: createGraph (V,{},S,T) in G .allSG()
set H = createGraph (V,{},S,T);
set H9 = the plain inducedSubgraph of G,V, {} ;
{} c= G .edgesBetween V by XBOOLE_1:2;
then A1: ( the_Vertices_of the plain inducedSubgraph of G,V, {} = V & the_Edges_of the plain inducedSubgraph of G,V, {} = {} ) by GLIB_000:def 37;
A2: ( the_Source_of the plain inducedSubgraph of G,V, {} = {} & the_Target_of the plain inducedSubgraph of G,V, {} = {} ) by A1;
( the_Vertices_of (createGraph (V,{},S,T)) = V & the_Edges_of (createGraph (V,{},S,T)) = {} & the_Source_of (createGraph (V,{},S,T)) = S & the_Target_of (createGraph (V,{},S,T)) = T ) ;
then createGraph (V,{},S,T) = the plain inducedSubgraph of G,V, {} by A1, A2, GLIB_000:def 34, GLIB_009:44;
hence createGraph (V,{},S,T) in G .allSG() by Th1; :: thesis: verum