let G1 be addAdjVertex of G,v1,e,v2; not 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 )
;
not G1 is connected
ex
u1,
u2 being
Vertex of
G1 st
for
W1 being
Walk of
G1 holds not
W1 is_Walk_from u1,
u2
proof
consider w1,
w2 being
Vertex of
G such that A2:
for
W being
Walk of
G holds not
W is_Walk_from w1,
w2
by GLIB_002:def 1;
reconsider u1 =
w1,
u2 =
w2 as
Vertex of
G1 by Th72;
take
u1
;
ex u2 being Vertex of G1 st
for W1 being Walk of G1 holds not W1 is_Walk_from u1,u2
take
u2
;
for W1 being Walk of G1 holds not W1 is_Walk_from u1,u2
let W1 be
Walk of
G1;
not W1 is_Walk_from u1,u2
assume A3:
W1 is_Walk_from u1,
u2
;
contradiction
set T = the
Trail of
W1;
(
W1 .first() = u1 &
W1 .last() = u2 )
by A3, GLIB_001:def 23;
then A4:
the
Trail of
W1 is_Walk_from u1,
u2
by GLIB_001:def 32;
then A5:
( the
Trail of
W1 .first() = w1 & the
Trail of
W1 .last() = w2 )
by GLIB_001:def 23;
w1 <> w2
then A6:
the
Trail of
W1 is
trivial
by A5, GLIB_001:127;
not
e in the
Trail of
W1 .edges()
by A1, A5, Th151;
then reconsider W = the
Trail of
W1 as
Walk of
G by A1, A6, Th149;
W is_Walk_from w1,
w2
by A4, GLIB_001:19;
hence
contradiction
by A2;
verum
end; hence
not
G1 is
connected
by GLIB_002:def 1;
verum suppose A7:
( not
v1 in the_Vertices_of G &
v2 in the_Vertices_of G & not
e in the_Edges_of G )
;
not G1 is connected
ex
u1,
u2 being
Vertex of
G1 st
for
W1 being
Walk of
G1 holds not
W1 is_Walk_from u1,
u2
proof
consider w1,
w2 being
Vertex of
G such that A8:
for
W being
Walk of
G holds not
W is_Walk_from w1,
w2
by GLIB_002:def 1;
reconsider u1 =
w1,
u2 =
w2 as
Vertex of
G1 by Th72;
take
u1
;
ex u2 being Vertex of G1 st
for W1 being Walk of G1 holds not W1 is_Walk_from u1,u2
take
u2
;
for W1 being Walk of G1 holds not W1 is_Walk_from u1,u2
let W1 be
Walk of
G1;
not W1 is_Walk_from u1,u2
assume A9:
W1 is_Walk_from u1,
u2
;
contradiction
set T = the
Trail of
W1;
(
W1 .first() = u1 &
W1 .last() = u2 )
by A9, GLIB_001:def 23;
then A10:
the
Trail of
W1 is_Walk_from u1,
u2
by GLIB_001:def 32;
then A11:
( the
Trail of
W1 .first() = w1 & the
Trail of
W1 .last() = w2 )
by GLIB_001:def 23;
w1 <> w2
then A12:
the
Trail of
W1 is
trivial
by A11, GLIB_001:127;
not
e in the
Trail of
W1 .edges()
by A7, A11, Th151;
then reconsider W = the
Trail of
W1 as
Walk of
G by A7, A12, Th150;
W is_Walk_from w1,
w2
by A10, GLIB_001:19;
hence
contradiction
by A8;
verum
end; hence
not
G1 is
connected
by GLIB_002:def 1;
verum