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

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

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

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

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

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 ;
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 ;