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

A3: now :: thesis: for x being Vertex of G1 st x <> v holds
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;

consider e being set such that
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

let v1, v2 be Vertex of G1; :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2

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

per cases ( v1 <> v or v1 = v ) ;

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;

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

per cases ( v2 <> v or v2 = v ) ;

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;

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;

end;

end;

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

end;

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

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

per cases ( v2 <> v or v2 = v ) ;

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;

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;

end;

end;

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

end;

end;

end;

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

end;

hence G1 is connected ; :: thesis: verum