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 holds

for v being Vertex of H st u = v holds

G .AdjacentSet {u} = H .AdjacentSet {v}

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 holds

for v being Vertex of H st u = v holds

G .AdjacentSet {u} = H .AdjacentSet {v}

let G2 be inducedSubgraph of G,S; :: thesis: for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds

for v being Vertex of G2 st u = v holds

G .AdjacentSet {u} = G2 .AdjacentSet {v}

let u be Vertex of G; :: thesis: ( u in S & G .AdjacentSet {u} c= S implies for v being Vertex of G2 st u = v holds

G .AdjacentSet {u} = G2 .AdjacentSet {v} )

assume that

A1: u in S and

A2: G .AdjacentSet {u} c= S ; :: thesis: for v being Vertex of G2 st u = v holds

G .AdjacentSet {u} = G2 .AdjacentSet {v}

let v be Vertex of G2; :: thesis: ( u = v implies G .AdjacentSet {u} = G2 .AdjacentSet {v} )

assume A3: u = v ; :: thesis: G .AdjacentSet {u} = G2 .AdjacentSet {v}

for H being inducedSubgraph of G,S

for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds

for v being Vertex of H st u = v holds

G .AdjacentSet {u} = H .AdjacentSet {v}

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 holds

for v being Vertex of H st u = v holds

G .AdjacentSet {u} = H .AdjacentSet {v}

let G2 be inducedSubgraph of G,S; :: thesis: for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds

for v being Vertex of G2 st u = v holds

G .AdjacentSet {u} = G2 .AdjacentSet {v}

let u be Vertex of G; :: thesis: ( u in S & G .AdjacentSet {u} c= S implies for v being Vertex of G2 st u = v holds

G .AdjacentSet {u} = G2 .AdjacentSet {v} )

assume that

A1: u in S and

A2: G .AdjacentSet {u} c= S ; :: thesis: for v being Vertex of G2 st u = v holds

G .AdjacentSet {u} = G2 .AdjacentSet {v}

let v be Vertex of G2; :: thesis: ( u = v implies G .AdjacentSet {u} = G2 .AdjacentSet {v} )

assume A3: u = v ; :: thesis: G .AdjacentSet {u} = G2 .AdjacentSet {v}

now :: thesis: for x being object holds

( ( x in G .AdjacentSet {u} implies x in G2 .AdjacentSet {v} ) & ( x in G2 .AdjacentSet {v} implies x in G .AdjacentSet {u} ) )

hence
G .AdjacentSet {u} = G2 .AdjacentSet {v}
by TARSKI:2; :: thesis: verum( ( x in G .AdjacentSet {u} implies x in G2 .AdjacentSet {v} ) & ( x in G2 .AdjacentSet {v} implies x in G .AdjacentSet {u} ) )

let x be object ; :: thesis: ( ( x in G .AdjacentSet {u} implies x in G2 .AdjacentSet {v} ) & ( x in G2 .AdjacentSet {v} implies x in G .AdjacentSet {u} ) )

then reconsider y = x as Vertex of G2 ;

x in the_Vertices_of G2 by A7;

then reconsider w = x as Vertex of G ;

y,v are_adjacent by A7, Th51;

then consider e being object such that

A8: e Joins y,v,G2 ;

e Joins y,v,G by A8, GLIB_000:72;

then A9: w,u are_adjacent by A3;

w <> u by A3, A7, Th51;

hence x in G .AdjacentSet {u} by A9, Th51; :: thesis: verum

end;hereby :: thesis: ( x in G2 .AdjacentSet {v} implies x in G .AdjacentSet {u} )

assume A7:
x in G2 .AdjacentSet {v}
; :: thesis: x in G .AdjacentSet {u}assume A4:
x in G .AdjacentSet {u}
; :: thesis: x in G2 .AdjacentSet {v}

then reconsider y = x as Vertex of G ;

reconsider w = x as Vertex of G2 by A2, A4, GLIB_000:def 37;

y,u are_adjacent by A4, Th51;

then consider e being object such that

A5: e Joins y,u,G ;

e Joins y,u,G2 by A1, A2, A4, A5, Th19;

then A6: w,v are_adjacent by A3;

w <> v by A3, A4, Th51;

hence x in G2 .AdjacentSet {v} by A6, Th51; :: thesis: verum

end;then reconsider y = x as Vertex of G ;

reconsider w = x as Vertex of G2 by A2, A4, GLIB_000:def 37;

y,u are_adjacent by A4, Th51;

then consider e being object such that

A5: e Joins y,u,G ;

e Joins y,u,G2 by A1, A2, A4, A5, Th19;

then A6: w,v are_adjacent by A3;

w <> v by A3, A4, Th51;

hence x in G2 .AdjacentSet {v} by A6, Th51; :: thesis: verum

then reconsider y = x as Vertex of G2 ;

x in the_Vertices_of G2 by A7;

then reconsider w = x as Vertex of G ;

y,v are_adjacent by A7, Th51;

then consider e being object such that

A8: e Joins y,v,G2 ;

e Joins y,v,G by A8, GLIB_000:72;

then A9: w,u are_adjacent by A3;

w <> u by A3, A7, Th51;

hence x in G .AdjacentSet {u} by A9, Th51; :: thesis: verum