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 )
S = the_Vertices_of H by GLIB_000:def 37;
hence ( u,v are_adjacent implies t,w are_adjacent ) by A1, A2, Th19; :: thesis: ( t,w are_adjacent implies u,v are_adjacent )
assume t,w are_adjacent ; :: thesis: u,v are_adjacent
then consider e being object such that
A3: e Joins t,w,H ;
e Joins u,v,G by A1, A2, A3, GLIB_000:72;
hence u,v are_adjacent ; :: thesis: verum