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

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