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

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