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 & G .AdjacentSet {u} c= S ) and
A2: 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 A3: u = v ; :: thesis: for Ga being AdjGraph of G,{u}
for Ha being AdjGraph of H,{v} holds Ga == Ha
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
A4: G .AdjacentSet {u} = H .AdjacentSet {v} by A1, A3, Th58;
Ga is inducedSubgraph of G,(G .AdjacentSet {u}) by Def5;
then A5: ( the_Vertices_of Ga = G .AdjacentSet {u} & the_Edges_of Ga = G .edgesBetween (G .AdjacentSet {u}) ) by A2, GLIB_000:def 39;
A6: Ha is inducedSubgraph of H,(H .AdjacentSet {v}) by Def5;
then A7: ( the_Edges_of Ha = H .edgesBetween (H .AdjacentSet {v}) & the_Vertices_of Ha = H .AdjacentSet {v} ) by A2, A4, GLIB_000:def 39;
thus the_Vertices_of Ga = the_Vertices_of Ha by A4, A5, A6, GLIB_000:def 39; :: according to GLIB_000:def 36 :: 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 )
thus A8: the_Edges_of Ga = the_Edges_of Ha by A1, A4, A5, A7, Th31; :: thesis: ( the_Source_of Ga = the_Source_of Ha & the_Target_of Ga = the_Target_of Ha )
A9: ( the_Source_of Ga = (the_Source_of G) | (the_Edges_of Ga) & the_Target_of Ga = (the_Target_of G) | (the_Edges_of Ga) ) by GLIB_000:48;
Ha is inducedSubgraph of H,(G .AdjacentSet {u}) by A4, Def5;
then Ha is inducedSubgraph of G,(G .AdjacentSet {u}) by A1, A2, Th29;
hence ( the_Source_of Ha = the_Source_of Ga & the_Target_of Ha = the_Target_of Ga ) by A8, A9, GLIB_000:48; :: thesis: verum