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 ;

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 Def37;
then A2: the_Edges_of G2 = the_Edges_of G1 by A1, Th34;
G1 is Subgraph of G1 by Lm3;
hence G1 == G2 by A1, A2, Th86; :: thesis: verum

end;

suppose V is not non empty Subset of (the_Vertices_of G1) ; :: thesis: G1 == G2

hence G1 == G2 by Def37; :: thesis: verum

end;

end;