let G2 be _Graph; for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
for W being Walk of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & ( ( not e in W .edges() & W is V5() ) or not v1 in W .vertices() ) holds
W is Walk of G2
let v1, e be object ; for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
for W being Walk of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & ( ( not e in W .edges() & W is V5() ) or not v1 in W .vertices() ) holds
W is Walk of G2
let v2 be Vertex of G2; for G1 being addAdjVertex of G2,v1,e,v2
for W being Walk of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & ( ( not e in W .edges() & W is V5() ) or not v1 in W .vertices() ) holds
W is Walk of G2
let G1 be addAdjVertex of G2,v1,e,v2; for W being Walk of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & ( ( not e in W .edges() & W is V5() ) or not v1 in W .vertices() ) holds
W is Walk of G2
let W be Walk of G1; ( not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & ( ( not e in W .edges() & W is V5() ) or not v1 in W .vertices() ) implies W is Walk of G2 )
assume that
A1:
( not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 )
and
A2:
( ( not e in W .edges() & W is V5() ) or not v1 in W .vertices() )
; W is Walk of G2
reconsider w = v1, e1 = e as set by TARSKI:1;
per cases
( ( not e in W .edges() & W is V5() ) or not v1 in W .vertices() )
by A2;
suppose A3:
( not
e in W .edges() &
W is
V5() )
;
W is Walk of G2consider G3 being
addVertex of
G2,
v1 such that A4:
G1 is
addEdge of
G3,
v1,
e,
v2
by A1, Th130;
A5:
not
e in the_Edges_of G3
by A1, Def10;
A6:
v2 is
Vertex of
G3
by Th72;
v1 is
Vertex of
G3
by Th98;
then
G3 is
removeEdge of
G1,
e1
by A4, A5, A6, Th112;
then reconsider W3 =
W as
Walk of
G3 by A3, GLIB_001:172;
W3 .vertices() misses {v1} \ (the_Vertices_of G2)
by A3, Th94;
hence
W is
Walk of
G2
by Th95;
verum end; end;