let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1
for v1, v2 being Vertex of G2 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 holds
v in W .vertices()
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1
for v1, v2 being Vertex of G2 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 holds
v in W .vertices()
let V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1
for v1, v2 being Vertex of G2 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 holds
v in W .vertices()
let G1 be addAdjVertexAll of G2,v,V; :: thesis: for W being Walk of G1
for v1, v2 being Vertex of G2 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 holds
v in W .vertices()
let W be Walk of G1; :: thesis: for v1, v2 being Vertex of G2 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 holds
v in W .vertices()
let v1, v2 be Vertex of G2; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 implies v in W .vertices() )
assume that
A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) and
A2: ( W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 ) ; :: thesis: v in W .vertices()
assume not v in W .vertices() ; :: thesis: contradiction
then reconsider W2 = W as Walk of G2 by A1, Th64;
( W2 .first() = v1 & W2 .last() = v2 ) by A2, GLIB_001:16;
then W2 is_Walk_from v1,v2 by GLIB_001:def 23;
hence contradiction by A2, GLIB_002:def 5; :: thesis: verum