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 A1: ( G2 is connected & ex e being set st
( e in v .edgesInOut() & not e Joins v,v,G1 ) ) ; :: thesis: G1 is connected
then consider e being set such that
A2: ( e in v .edgesInOut() & not e Joins v,v,G1 ) ;

A3: now

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:50; :: thesis: verum

end;

set v3 = v .adj e;
v <> v .adj e by A2, GLIB_000:70;
then reconsider v3' = v .adj e as Vertex of G2 by A3;
A4: e Joins v,v .adj e,G1 by A2, GLIB_000:70;
then A5: e Joins v .adj e,v,G1 by GLIB_000:17;

now

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

now

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 v1' = v1 as Vertex of G2 by A3;

now

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 v2' = v2 as Vertex of G2 by A3;
consider W' being Walk of G2 such that
A6: W' is_Walk_from v1',v2' by A1, Def1;
reconsider W = W' as Walk of G1 by GLIB_001:168;
W is_Walk_from v1,v2 by A6, GLIB_001:20;
hence ex W being Walk of G1 st W is_Walk_from v1,v2 ; :: thesis: verum

end;

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

consider W' being Walk of G2 such that
A8: W' is_Walk_from v1',v3' by A1, Def1;
reconsider W = W' as Walk of G1 by GLIB_001:168;
W is_Walk_from v1,v .adj e by A8, GLIB_001:20;
then ( W .first() = v1 & W .last() = v .adj e ) by GLIB_001:def 23;
then W .addEdge e is_Walk_from v1,v2 by A5, A7, GLIB_001:64;
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 A9: v1 = v ; :: thesis: ex W being Walk of G1 st W is_Walk_from v1,v2

now

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 v2' = v2 as Vertex of G2 by A3;
set W1 = G1 .walkOf v1,e,(v .adj e);
A10: G1 .walkOf v1,e,(v .adj e) is_Walk_from v1,v .adj e by A4, A9, GLIB_001:16;
consider W2' being Walk of G2 such that
A11: W2' is_Walk_from v3',v2' by A1, Def1;
reconsider W2 = W2' as Walk of G1 by GLIB_001:168;
A12: W2 is_Walk_from v .adj e,v2 by A11, GLIB_001:20;
take W = (G1 .walkOf v1,e,(v .adj e)) .append W2; :: thesis: W is_Walk_from v1,v2
thus W is_Walk_from v1,v2 by A10, A12, GLIB_001:32; :: thesis: verum

end;

suppose A13: 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 A9, A13, GLIB_001:14; :: 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 by Def1; :: thesis: verum