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 holds
for v being Vertex of H st u = v holds
G .AdjacentSet {u} = H .AdjacentSet {v}

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 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:
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 ;
y,u are_adjacent by ;
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 ; :: thesis: verum
end;
assume A7: x in G2 .AdjacentSet {v} ; :: thesis:
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 ;
then consider e being object such that
A8: e Joins y,v,G2 ;
e Joins y,v,G by ;
then A9: w,u are_adjacent by A3;
w <> u by A3, A7, Th51;
hence x in G .AdjacentSet {u} by ; :: thesis: verum
end;
hence G .AdjacentSet {u} = G2 .AdjacentSet {v} by TARSKI:2; :: thesis: verum