let G1 be non _trivial _Graph; :: thesis: for v being Vertex of G1

for G2 being removeVertex of G1,v st G2 is connected & ex e being set st

( e in v .edgesInOut() & not e Joins v,v,G1 ) holds

G1 is connected

let v be Vertex of G1; :: thesis: for G2 being removeVertex of G1,v st G2 is connected & ex e being set st

( e in v .edgesInOut() & not e Joins v,v,G1 ) holds

G1 is connected

let G2 be removeVertex of G1,v; :: thesis: ( G2 is connected & ex e being set st

( e in v .edgesInOut() & not e Joins v,v,G1 ) implies G1 is connected )

assume that

A1: G2 is connected and

A2: ex e being set st

( e in v .edgesInOut() & not e Joins v,v,G1 ) ; :: thesis: G1 is connected

A4: e in v .edgesInOut() and

A5: not e Joins v,v,G1 by A2;

set v3 = v .adj e;

v <> v .adj e by A4, A5, GLIB_000:67;

then reconsider v39 = v .adj e as Vertex of G2 by A3;

A6: e Joins v,v .adj e,G1 by A4, GLIB_000:67;

then A7: e Joins v .adj e,v,G1 by GLIB_000:14;

for G2 being removeVertex of G1,v st G2 is connected & ex e being set st

( e in v .edgesInOut() & not e Joins v,v,G1 ) holds

G1 is connected

let v be Vertex of G1; :: thesis: for G2 being removeVertex of G1,v st G2 is connected & ex e being set st

( e in v .edgesInOut() & not e Joins v,v,G1 ) holds

G1 is connected

let G2 be removeVertex of G1,v; :: thesis: ( G2 is connected & ex e being set st

( e in v .edgesInOut() & not e Joins v,v,G1 ) implies G1 is connected )

assume that

A1: G2 is connected and

A2: ex e being set st

( e in v .edgesInOut() & not e Joins v,v,G1 ) ; :: thesis: G1 is connected

A3: now :: thesis: for x being Vertex of G1 st x <> v holds

x in the_Vertices_of G2

consider e being set such that x in the_Vertices_of G2

let x be Vertex of G1; :: thesis: ( x <> v implies x in the_Vertices_of G2 )

assume x <> v ; :: thesis: x in the_Vertices_of G2

then not x in {v} by TARSKI:def 1;

then x in (the_Vertices_of G1) \ {v} by XBOOLE_0:def 5;

hence x in the_Vertices_of G2 by GLIB_000:47; :: thesis: verum

end;assume x <> v ; :: thesis: x in the_Vertices_of G2

then not x in {v} by TARSKI:def 1;

then x in (the_Vertices_of G1) \ {v} by XBOOLE_0:def 5;

hence x in the_Vertices_of G2 by GLIB_000:47; :: thesis: verum

A4: e in v .edgesInOut() and

A5: not e Joins v,v,G1 by A2;

set v3 = v .adj e;

v <> v .adj e by A4, A5, GLIB_000:67;

then reconsider v39 = v .adj e as Vertex of G2 by A3;

A6: e Joins v,v .adj e,G1 by A4, GLIB_000:67;

then A7: e Joins v .adj e,v,G1 by GLIB_000:14;

now :: thesis: for v1, v2 being Vertex of G1 ex W being Walk of G1 st W is_Walk_from v1,v2

hence
G1 is connected
; :: thesis: verumlet v1, v2 be Vertex of G1; :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2

end;now :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2end;

hence
ex W being Walk of G1 st W is_Walk_from v1,v2
; :: thesis: verumper cases
( v1 <> v or v1 = v )
;

end;

suppose
v1 <> v
; :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2

then reconsider v19 = v1 as Vertex of G2 by A3;

end;now :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2end;

hence
ex W being Walk of G1 st W is_Walk_from v1,v2
; :: thesis: verumper cases
( v2 <> v or v2 = v )
;

end;

suppose
v2 <> v
; :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2

then reconsider v29 = v2 as Vertex of G2 by A3;

consider W9 being Walk of G2 such that

A8: W9 is_Walk_from v19,v29 by A1;

reconsider W = W9 as Walk of G1 by GLIB_001:167;

W is_Walk_from v1,v2 by A8, GLIB_001:19;

hence ex W being Walk of G1 st W is_Walk_from v1,v2 ; :: thesis: verum

end;consider W9 being Walk of G2 such that

A8: W9 is_Walk_from v19,v29 by A1;

reconsider W = W9 as Walk of G1 by GLIB_001:167;

W is_Walk_from v1,v2 by A8, GLIB_001:19;

hence ex W being Walk of G1 st W is_Walk_from v1,v2 ; :: thesis: verum

suppose A9:
v2 = v
; :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2

consider W9 being Walk of G2 such that

A10: W9 is_Walk_from v19,v39 by A1;

reconsider W = W9 as Walk of G1 by GLIB_001:167;

W is_Walk_from v1,v .adj e by A10, GLIB_001:19;

then ( W .first() = v1 & W .last() = v .adj e ) by GLIB_001:def 23;

then W .addEdge e is_Walk_from v1,v2 by A7, A9, GLIB_001:63;

hence ex W being Walk of G1 st W is_Walk_from v1,v2 ; :: thesis: verum

end;A10: W9 is_Walk_from v19,v39 by A1;

reconsider W = W9 as Walk of G1 by GLIB_001:167;

W is_Walk_from v1,v .adj e by A10, GLIB_001:19;

then ( W .first() = v1 & W .last() = v .adj e ) by GLIB_001:def 23;

then W .addEdge e is_Walk_from v1,v2 by A7, A9, GLIB_001:63;

hence ex W being Walk of G1 st W is_Walk_from v1,v2 ; :: thesis: verum

suppose A11:
v1 = v
; :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2

end;

now :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2end;

hence
ex W being Walk of G1 st W is_Walk_from v1,v2
; :: thesis: verumper cases
( v2 <> v or v2 = v )
;

end;

suppose
v2 <> v
; :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2

then reconsider v29 = v2 as Vertex of G2 by A3;

set W1 = G1 .walkOf (v1,e,(v .adj e));

consider W29 being Walk of G2 such that

A12: W29 is_Walk_from v39,v29 by A1;

reconsider W2 = W29 as Walk of G1 by GLIB_001:167;

A13: W2 is_Walk_from v .adj e,v2 by A12, GLIB_001:19;

take W = (G1 .walkOf (v1,e,(v .adj e))) .append W2; :: thesis: W is_Walk_from v1,v2

G1 .walkOf (v1,e,(v .adj e)) is_Walk_from v1,v .adj e by A6, A11, GLIB_001:15;

hence W is_Walk_from v1,v2 by A13, GLIB_001:31; :: thesis: verum

end;set W1 = G1 .walkOf (v1,e,(v .adj e));

consider W29 being Walk of G2 such that

A12: W29 is_Walk_from v39,v29 by A1;

reconsider W2 = W29 as Walk of G1 by GLIB_001:167;

A13: W2 is_Walk_from v .adj e,v2 by A12, GLIB_001:19;

take W = (G1 .walkOf (v1,e,(v .adj e))) .append W2; :: thesis: W is_Walk_from v1,v2

G1 .walkOf (v1,e,(v .adj e)) is_Walk_from v1,v .adj e by A6, A11, GLIB_001:15;

hence W is_Walk_from v1,v2 by A13, GLIB_001:31; :: thesis: verum

suppose A14:
v2 = v
; :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2

take W = G1 .walkOf v; :: thesis: W is_Walk_from v1,v2

thus W is_Walk_from v1,v2 by A11, A14, GLIB_001:13; :: thesis: verum

end;thus W is_Walk_from v1,v2 by A11, A14, GLIB_001:13; :: thesis: verum