let G1 be addVertices of G,V; :: thesis: not G1 is connected
ex u1, v1 being Vertex of G1 st
for W being Walk of G1 holds not W is_Walk_from u1,v1
proof
consider u, v being Vertex of G such that
A1: for W being Walk of G holds not W is_Walk_from u,v by GLIB_002:def 1;
reconsider u1 = u, v1 = v as Vertex of G1 by Th72;
take u1 ; :: thesis: ex v1 being Vertex of G1 st
for W being Walk of G1 holds not W is_Walk_from u1,v1
take v1 ; :: thesis: for W being Walk of G1 holds not W is_Walk_from u1,v1
let W be Walk of G1; :: thesis: not W is_Walk_from u1,v1
assume A2: W is_Walk_from u1,v1 ; :: thesis: contradiction
per cases ( W .vertices() misses V \ (the_Vertices_of G) or not W is V5() ) by Th94;
suppose W .vertices() misses V \ (the_Vertices_of G) ; :: thesis: contradiction
then reconsider W2 = W as Walk of G by Th95;
W2 is_Walk_from u,v by A2, GLIB_001:19;
hence contradiction by A1; :: thesis: verum
end;
suppose W is V5() ; :: thesis: contradiction
then consider w being Vertex of G1 such that
A4: W = G1 .walkOf w by GLIB_001:128;
( W .first() = u1 & W .last() = v1 ) by A2, GLIB_001:def 23;
then ( u1 = w & v1 = w ) by A4, GLIB_001:13;
then G .walkOf v is_Walk_from u,v by GLIB_001:13;
hence contradiction by A1; :: thesis: verum
end;
end;
end;
hence not G1 is connected by GLIB_002:def 1; :: thesis: verum