let G be _Graph; :: thesis: for S being non empty Subset of ()
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 (); :: 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,() by Def5;
A6: Ga is inducedSubgraph of G,() by Def5;
then A7: the_Edges_of Ga = G .edgesBetween () by ;
the_Vertices_of Ga = G .AdjacentSet {u} by ;
hence the_Vertices_of Ga = the_Vertices_of Ha by ; :: according to GLIB_000:def 34 :: thesis:
the_Edges_of Ha = H .edgesBetween () by ;
hence A8: the_Edges_of Ga = the_Edges_of Ha by A2, A3, A4, A7, Th31; :: thesis:
A9: the_Target_of Ga = () | () by GLIB_000:45;
Ha is inducedSubgraph of H,() by ;
then A10: Ha is inducedSubgraph of G,() by A2, A3, Th29;
the_Source_of Ga = () | () by GLIB_000:45;
hence ( the_Source_of Ha = the_Source_of Ga & the_Target_of Ha = the_Target_of Ga ) by ; :: thesis: verum