let G1 be addAdjVertex of G,v1,e,v2; G1 is connected
per cases
( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ) )
;
suppose A1:
(
v1 in the_Vertices_of G & not
v2 in the_Vertices_of G & not
e in the_Edges_of G )
;
G1 is connected
for
u1,
u2 being
Vertex of
G1 ex
W1 being
Walk of
G1 st
W1 is_Walk_from u1,
u2
proof
let u1,
u2 be
Vertex of
G1;
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2
per cases
( u1 in the_Vertices_of G or not u1 in the_Vertices_of G )
;
suppose
u1 in the_Vertices_of G
;
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2then reconsider w1 =
u1 as
Vertex of
G ;
per cases
( u2 in the_Vertices_of G or not u2 in the_Vertices_of G )
;
suppose A3:
not
u2 in the_Vertices_of G
;
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2
the_Vertices_of G1 = (the_Vertices_of G) \/ {v2}
by A1, Def12;
then
u2 in {v2}
by A3, XBOOLE_0:def 3;
then
u2 = v2
by TARSKI:def 1;
then A4:
e Joins v1,
u2,
G1
by A1, Th135;
reconsider w2 =
v1 as
Vertex of
G by A1;
consider W2 being
Walk of
G such that A5:
W2 is_Walk_from w1,
w2
by GLIB_002:def 1;
reconsider W =
W2 as
Walk of
G1 by Th79;
W is_Walk_from u1,
v1
by A5, GLIB_001:19;
then A6:
(
W .first() = u1 &
W .last() = v1 )
by GLIB_001:def 23;
set W1 =
W .addEdge e;
take
W .addEdge e
;
W .addEdge e is_Walk_from u1,u2thus
W .addEdge e is_Walk_from u1,
u2
by A4, A6, GLIB_001:63;
verum end; end; end; suppose A7:
not
u1 in the_Vertices_of G
;
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2A8:
the_Vertices_of G1 = (the_Vertices_of G) \/ {v2}
by A1, Def12;
then
u1 in {v2}
by A7, XBOOLE_0:def 3;
then A9:
u1 = v2
by TARSKI:def 1;
then
e DJoins v1,
u1,
G1
by A1, Th135;
then A10:
e Joins u1,
v1,
G1
by GLIB_000:16;
per cases
( u2 in the_Vertices_of G or not u2 in the_Vertices_of G )
;
suppose
u2 in the_Vertices_of G
;
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2then reconsider w2 =
u2 as
Vertex of
G ;
reconsider w1 =
v1 as
Vertex of
G by A1;
consider W2 being
Walk of
G such that A11:
W2 is_Walk_from w1,
w2
by GLIB_002:def 1;
reconsider W =
W2 as
Walk of
G1 by Th79;
W is_Walk_from v1,
u2
by A11, GLIB_001:19;
then A12:
(
W .first() = v1 &
W .last() = u2 )
by GLIB_001:def 23;
set W3 =
G1 .walkOf (
u1,
e,
v1);
A13:
(
(G1 .walkOf (u1,e,v1)) .first() = u1 &
(G1 .walkOf (u1,e,v1)) .last() = v1 )
by A10, GLIB_001:15;
set W1 =
(G1 .walkOf (u1,e,v1)) .append W;
take
(G1 .walkOf (u1,e,v1)) .append W
;
(G1 .walkOf (u1,e,v1)) .append W is_Walk_from u1,u2thus
(G1 .walkOf (u1,e,v1)) .append W is_Walk_from u1,
u2
by A12, A13, GLIB_001:30;
verum end; end; end; end;
end; hence
G1 is
connected
by GLIB_002:def 1;
verum end; suppose A15:
( not
v1 in the_Vertices_of G &
v2 in the_Vertices_of G & not
e in the_Edges_of G )
;
G1 is connected
for
u1,
u2 being
Vertex of
G1 ex
W1 being
Walk of
G1 st
W1 is_Walk_from u1,
u2
proof
let u1,
u2 be
Vertex of
G1;
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2
per cases
( u1 in the_Vertices_of G or not u1 in the_Vertices_of G )
;
suppose
u1 in the_Vertices_of G
;
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2then reconsider w1 =
u1 as
Vertex of
G ;
per cases
( u2 in the_Vertices_of G or not u2 in the_Vertices_of G )
;
suppose A17:
not
u2 in the_Vertices_of G
;
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2
the_Vertices_of G1 = (the_Vertices_of G) \/ {v1}
by A15, Def12;
then
u2 in {v1}
by A17, XBOOLE_0:def 3;
then
u2 = v1
by TARSKI:def 1;
then
e DJoins u2,
v2,
G1
by A15, Th136;
then A18:
e Joins v2,
u2,
G1
by GLIB_000:16;
reconsider w2 =
v2 as
Vertex of
G by A15;
consider W2 being
Walk of
G such that A19:
W2 is_Walk_from w1,
w2
by GLIB_002:def 1;
reconsider W =
W2 as
Walk of
G1 by Th79;
W is_Walk_from u1,
v2
by A19, GLIB_001:19;
then A20:
(
W .first() = u1 &
W .last() = v2 )
by GLIB_001:def 23;
set W1 =
W .addEdge e;
take
W .addEdge e
;
W .addEdge e is_Walk_from u1,u2thus
W .addEdge e is_Walk_from u1,
u2
by A18, A20, GLIB_001:63;
verum end; end; end; suppose A21:
not
u1 in the_Vertices_of G
;
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2A22:
the_Vertices_of G1 = (the_Vertices_of G) \/ {v1}
by A15, Def12;
then
u1 in {v1}
by A21, XBOOLE_0:def 3;
then A23:
u1 = v1
by TARSKI:def 1;
then A24:
e Joins u1,
v2,
G1
by A15, Th136;
per cases
( u2 in the_Vertices_of G or not u2 in the_Vertices_of G )
;
suppose
u2 in the_Vertices_of G
;
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2then reconsider w2 =
u2 as
Vertex of
G ;
reconsider w1 =
v2 as
Vertex of
G by A15;
consider W2 being
Walk of
G such that A25:
W2 is_Walk_from w1,
w2
by GLIB_002:def 1;
reconsider W =
W2 as
Walk of
G1 by Th79;
W is_Walk_from v2,
u2
by A25, GLIB_001:19;
then A26:
(
W .first() = v2 &
W .last() = u2 )
by GLIB_001:def 23;
set W3 =
G1 .walkOf (
u1,
e,
v2);
A27:
(
(G1 .walkOf (u1,e,v2)) .first() = u1 &
(G1 .walkOf (u1,e,v2)) .last() = v2 )
by A24, GLIB_001:15;
set W1 =
(G1 .walkOf (u1,e,v2)) .append W;
take
(G1 .walkOf (u1,e,v2)) .append W
;
(G1 .walkOf (u1,e,v2)) .append W is_Walk_from u1,u2thus
(G1 .walkOf (u1,e,v2)) .append W is_Walk_from u1,
u2
by A26, A27, GLIB_001:30;
verum end; end; end; end;
end; hence
G1 is
connected
by GLIB_002:def 1;
verum end; end;