let G2 be _Graph; for V being set
for G1 being addLoops of G2,V holds
( G1 is connected iff G2 is connected )
let V be set ; for G1 being addLoops of G2,V holds
( G1 is connected iff G2 is connected )
let G1 be addLoops of G2,V; ( G1 is connected iff G2 is connected )
hereby ( G2 is connected implies G1 is connected )
assume A1:
G1 is
connected
;
G2 is connected now for u, v being Vertex of G2 ex P2 being Walk of G2 st P2 is_Walk_from u,vlet u,
v be
Vertex of
G2;
ex P2 being Walk of G2 st b3 is_Walk_from P2,b2
(
u is
Vertex of
G1 &
v is
Vertex of
G1 )
by Th15;
then consider W1 being
Walk of
G1 such that A2:
W1 is_Walk_from u,
v
by A1, GLIB_002:def 1;
set P1 = the
Path of
W1;
per cases
( the Path of W1 is Path of G2 or ex w, e being object st
( e Joins w,w,G1 & the Path of W1 = G1 .walkOf (w,e,w) ) )
by Th37;
suppose
ex
w,
e being
object st
(
e Joins w,
w,
G1 & the
Path of
W1 = G1 .walkOf (
w,
e,
w) )
;
ex W2 being Walk of G2 st b3 is_Walk_from W2,b2then consider w,
e being
object such that A3:
(
e Joins w,
w,
G1 & the
Path of
W1 = G1 .walkOf (
w,
e,
w) )
;
A4:
( the
Path of
W1 .first() = w & the
Path of
W1 .last() = w )
by A3, GLIB_001:15;
the
Path of
W1 is_Walk_from u,
v
by A2, GLIB_001:160;
then A5:
( the
Path of
W1 .first() = u & the
Path of
W1 .last() = v )
by GLIB_001:def 23;
reconsider W2 =
G2 .walkOf u as
Walk of
G2 ;
take W2 =
W2;
W2 is_Walk_from u,vthus
W2 is_Walk_from u,
v
by A4, A5, GLIB_001:13;
verum end; end; end; hence
G2 is
connected
by GLIB_002:def 1;
verum
end;
assume A6:
G2 is connected
; G1 is connected
hence
G1 is connected
by GLIB_002:def 1; verum