let G2 be _Graph; for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not G2 is connected & v2 in G2 .reachableFrom v1 holds
not G1 is connected
let v1, v2 be Vertex of G2; for e being object
for G1 being addEdge of G2,v1,e,v2 st not G2 is connected & v2 in G2 .reachableFrom v1 holds
not G1 is connected
let e be object ; for G1 being addEdge of G2,v1,e,v2 st not G2 is connected & v2 in G2 .reachableFrom v1 holds
not G1 is connected
let G1 be addEdge of G2,v1,e,v2; ( not G2 is connected & v2 in G2 .reachableFrom v1 implies not G1 is connected )
assume that
A1:
not G2 is connected
and
A2:
v2 in G2 .reachableFrom v1
; not G1 is connected
per cases
( ( v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) or not v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 )
;
suppose A3:
(
v1 in the_Vertices_of G2 &
v2 in the_Vertices_of G2 & not
e in the_Edges_of G2 )
;
not G1 is connected
ex
u,
v being
Vertex of
G1 st
for
W being
Walk of
G1 holds not
W is_Walk_from u,
v
proof
assume A4:
for
u,
v being
Vertex of
G1 ex
W being
Walk of
G1 st
W is_Walk_from u,
v
;
contradiction
consider u,
v being
Vertex of
G2 such that A5:
for
W being
Walk of
G2 holds not
W is_Walk_from u,
v
by A1, GLIB_002:def 1;
reconsider u1 =
u,
v3 =
v as
Vertex of
G1 by Th72;
consider W1 being
Walk of
G1 such that A6:
W1 is_Walk_from u1,
v3
by A4;
set T = the
Trail of
W1;
A7:
the
Trail of
W1 is_Walk_from u1,
v3
by A6, GLIB_001:160;
per cases
( not e in the Trail of W1 .edges() or e in the Trail of W1 .edges() )
;
suppose
e in the
Trail of
W1 .edges()
;
contradictionthen consider w1,
w2 being
Vertex of
G1,
n being
odd Element of
NAT such that A9:
n + 2
<= len the
Trail of
W1
and A10:
(
w1 = the
Trail of
W1 . n &
e = the
Trail of
W1 . (n + 1) &
w2 = the
Trail of
W1 . (n + 2) )
and A11:
e Joins w1,
w2,
G1
by GLIB_001:103;
set E =
G1 .walkOf (
w1,
e,
w2);
A12:
G1 .walkOf (
w1,
e,
w2)
is_odd_substring_of the
Trail of
W1,
0
by A9, A10, Th31;
e DJoins v1,
v2,
G1
by A3, Th109;
then A13:
e Joins v1,
v2,
G1
by GLIB_000:16;
per cases then
( ( v1 = w1 & v2 = w2 ) or ( v1 = w2 & v2 = w1 ) )
by A11, GLIB_000:15;
suppose A14:
(
v1 = w1 &
v2 = w2 )
;
contradictionconsider W2 being
Walk of
G2 such that A15:
W2 is_Walk_from v1,
v2
by A2, GLIB_002:def 5;
reconsider W4 =
W2 as
Walk of
G1 by Th79;
not
e in W2 .edges()
by A3;
then A16:
not
e in W4 .edges()
by GLIB_001:110;
set W5 = the
Trail of
W1 .replaceEdgeWith (
e,
W4);
A17:
the
Trail of
W1 .replaceEdgeWith (
e,
W4)
is_Walk_from u1,
v3
by A7, Th51;
(
W2 .first() = v1 &
W2 .last() = v2 )
by A15, GLIB_001:def 23;
then A18:
(
W4 .first() = v1 &
W4 .last() = v2 )
by GLIB_001:16;
G1 .walkOf (
(W4 .first()),
e,
(W4 .last()))
is_odd_substring_of the
Trail of
W1,
0
by A12, A14, A18;
then
not
e in ( the Trail of W1 .replaceEdgeWith (e,W4)) .edges()
by A13, A16, A18, Th44;
then reconsider W = the
Trail of
W1 .replaceEdgeWith (
e,
W4) as
Walk of
G2 by Th113;
W is_Walk_from u,
v
by A17, GLIB_001:19;
hence
contradiction
by A5;
verum end; suppose A21:
(
v1 = w2 &
v2 = w1 )
;
contradictionconsider W3 being
Walk of
G2 such that A22:
W3 is_Walk_from v1,
v2
by A2, GLIB_002:def 5;
set W2 =
W3 .reverse() ;
A23:
W3 .reverse() is_Walk_from v2,
v1
by A22, GLIB_001:23;
reconsider W4 =
W3 .reverse() as
Walk of
G1 by Th79;
not
e in (W3 .reverse()) .edges()
by A3;
then A24:
not
e in W4 .edges()
by GLIB_001:110;
set W5 = the
Trail of
W1 .replaceEdgeWith (
e,
W4);
A25:
the
Trail of
W1 .replaceEdgeWith (
e,
W4)
is_Walk_from u1,
v3
by A7, Th51;
(
(W3 .reverse()) .first() = v2 &
(W3 .reverse()) .last() = v1 )
by A23, GLIB_001:def 23;
then A26:
(
W4 .first() = v2 &
W4 .last() = v1 )
by GLIB_001:16;
G1 .walkOf (
(W4 .first()),
e,
(W4 .last()))
is_odd_substring_of the
Trail of
W1,
0
by A12, A21, A26;
then
not
e in ( the Trail of W1 .replaceEdgeWith (e,W4)) .edges()
by A13, A24, A26, Th44, GLIB_000:14;
then reconsider W = the
Trail of
W1 .replaceEdgeWith (
e,
W4) as
Walk of
G2 by Th113;
W is_Walk_from u,
v
by A25, GLIB_001:19;
hence
contradiction
by A5;
verum end; end;
end; hence
not
G1 is
connected
by GLIB_002:def 1;
verum