let G be _Graph; :: thesis: for S being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for u being Vertex of G st u in S & G .AdjacentSet {u} c= S & G .AdjacentSet {u} <> {} holds
for v being Vertex of H st u = v holds
for Ga being AdjGraph of G,{u}
for Ha being AdjGraph of H,{v} holds Ga == Ha
let S be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,S
for u being Vertex of G st u in S & G .AdjacentSet {u} c= S & G .AdjacentSet {u} <> {} holds
for v being Vertex of H st u = v holds
for Ga being AdjGraph of G,{u}
for Ha being AdjGraph of H,{v} holds Ga == Ha
let H be inducedSubgraph of G,S; :: thesis: for u being Vertex of G st u in S & G .AdjacentSet {u} c= S & G .AdjacentSet {u} <> {} holds
for v being Vertex of H st u = v holds
for Ga being AdjGraph of G,{u}
for Ha being AdjGraph of H,{v} holds Ga == Ha
let u be Vertex of G; :: thesis: ( u in S & G .AdjacentSet {u} c= S & G .AdjacentSet {u} <> {} implies for v being Vertex of H st u = v holds
for Ga being AdjGraph of G,{u}
for Ha being AdjGraph of H,{v} holds Ga == Ha )
assume that
A1: u in S and
A2: G .AdjacentSet {u} c= S and
A3: G .AdjacentSet {u} <> {} ; :: thesis: for v being Vertex of H st u = v holds
for Ga being AdjGraph of G,{u}
for Ha being AdjGraph of H,{v} holds Ga == Ha
let v be Vertex of H; :: thesis: ( u = v implies for Ga being AdjGraph of G,{u}
for Ha being AdjGraph of H,{v} holds Ga == Ha )
assume u = v ; :: thesis: for Ga being AdjGraph of G,{u}
for Ha being AdjGraph of H,{v} holds Ga == Ha
then A4: G .AdjacentSet {u} = H .AdjacentSet {v} by A1, A2, Th57;
let Ga be AdjGraph of G,{u}; :: thesis: for Ha being AdjGraph of H,{v} holds Ga == Ha
let Ha be AdjGraph of H,{v}; :: thesis: Ga == Ha
A5: Ha is inducedSubgraph of H,(H .AdjacentSet {v}) by Def5;
A6: Ga is inducedSubgraph of G,(G .AdjacentSet {u}) by Def5;
then A7: the_Edges_of Ga = G .edgesBetween (G .AdjacentSet {u}) by A3, GLIB_000:def 37;
the_Vertices_of Ga = G .AdjacentSet {u} by A3, A6, GLIB_000:def 37;
hence the_Vertices_of Ga = the_Vertices_of Ha by A4, A5, GLIB_000:def 37; :: according to GLIB_000:def 34 :: thesis: ( the_Edges_of Ga = the_Edges_of Ha & the_Source_of Ga = the_Source_of Ha & the_Target_of Ga = the_Target_of Ha )
the_Edges_of Ha = H .edgesBetween (H .AdjacentSet {v}) by A3, A4, A5, GLIB_000:def 37;
hence A8: the_Edges_of Ga = the_Edges_of Ha by A2, A3, A4, A7, Th31; :: thesis: ( the_Source_of Ga = the_Source_of Ha & the_Target_of Ga = the_Target_of Ha )
A9: the_Target_of Ga = (the_Target_of G) | (the_Edges_of Ga) by GLIB_000:45;
Ha is inducedSubgraph of H,(G .AdjacentSet {u}) by A4, Def5;
then A10: Ha is inducedSubgraph of G,(G .AdjacentSet {u}) by A2, A3, Th29;
the_Source_of Ga = (the_Source_of G) | (the_Edges_of Ga) by GLIB_000:45;
hence ( the_Source_of Ha = the_Source_of Ga & the_Target_of Ha = the_Target_of Ga ) by A8, A9, A10, GLIB_000:45; :: thesis: verum