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}

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} ) )

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} ) )

hereby :: thesis: ( x in G2 .AdjacentSet {v} implies 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;

assume A7: x in G2 .AdjacentSet {v} ; :: thesis: 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;

hence G .AdjacentSet {u} = G2 .AdjacentSet {v} by TARSKI:2; :: thesis: verum