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, v being Vertex of G
for t, w being Vertex of H st u = t & v = w holds
( u,v are_adjacent iff t,w are_adjacent )
let S be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,S
for u, v being Vertex of G
for t, w being Vertex of H st u = t & v = w holds
( u,v are_adjacent iff t,w are_adjacent )
let H be inducedSubgraph of G,S; :: thesis: for u, v being Vertex of G
for t, w being Vertex of H st u = t & v = w holds
( u,v are_adjacent iff t,w are_adjacent )
let u, v be Vertex of G; :: thesis: for t, w being Vertex of H st u = t & v = w holds
( u,v are_adjacent iff t,w are_adjacent )
let t, w be Vertex of H; :: thesis: ( u = t & v = w implies ( u,v are_adjacent iff t,w are_adjacent ) )
assume that
A1: u = t and
A2: v = w ; :: thesis: ( u,v are_adjacent iff t,w are_adjacent )
A3: S = the_Vertices_of H by GLIB_000:def 39;

hereby :: thesis: ( t,w are_adjacent implies u,v are_adjacent )

assume u,v are_adjacent ; :: thesis: t,w are_adjacent
then consider e being set such that
A4: e Joins u,v,G by Def3;
e Joins t,w,H by A1, A2, A3, A4, Th19;
hence t,w are_adjacent by Def3; :: thesis: verum

end;

assume t,w are_adjacent ; :: thesis: u,v are_adjacent
then consider e being set such that
A5: e Joins t,w,H by Def3;
e Joins u,v,G by A1, A2, A5, GLIB_000:75;
hence u,v are_adjacent by Def3; :: thesis: verum