let G1 be _Graph; :: thesis: for V being set
for G2 being inducedSubgraph of G1,V st G2 is spanning holds
G1 == G2
let V be set ; :: thesis: for G2 being inducedSubgraph of G1,V st G2 is spanning holds
G1 == G2
let G2 be inducedSubgraph of G1,V; :: thesis: ( G2 is spanning implies G1 == G2 )
assume G2 is spanning ; :: thesis: G1 == G2
then A1: the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:def 33;
per cases ( V is non empty Subset of (the_Vertices_of G1) or not V is non empty Subset of (the_Vertices_of G1) ) ;
suppose V is non empty Subset of (the_Vertices_of G1) ; :: thesis: G1 == G2
then ( the_Vertices_of G2 = V & the_Edges_of G2 = G1 .edgesBetween V ) by GLIB_000:def 37;
then A2: the_Edges_of G2 = the_Edges_of G1 by A1, GLIB_000:34;
G1 is Subgraph of G1 by GLIB_000:40;
hence G1 == G2 by A1, A2, GLIB_000:86; :: thesis: verum
end;
suppose V is not non empty Subset of (the_Vertices_of G1) ; :: thesis: G1 == G2
hence G1 == G2 by GLIB_000:def 37; :: thesis: verum
end;
end;