let G2 be _Graph; :: thesis: for V being set
for G1 being addLoops of G2,V holds
( G1 is connected iff G2 is connected )
let V be set ; :: thesis: for G1 being addLoops of G2,V holds
( G1 is connected iff G2 is connected )
let G1 be addLoops of G2,V; :: thesis: ( G1 is connected iff G2 is connected )

hereby :: thesis: ( G2 is connected implies G1 is connected )

assume A1: G1 is connected ; :: thesis: G2 is connected

now :: thesis: for u, v being Vertex of G2 ex P2 being Walk of G2 st P2 is_Walk_from u,v

let u, v be Vertex of G2; :: thesis: ex P2 being Walk of G2 st b₃ is_Walk_from P2,b₂
( 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 the Path of W1 is Path of G2 ; :: thesis: ex P2 being Walk of G2 st b₃ is_Walk_from P2,b₂

then reconsider P2 = the Path of W1 as Walk of G2 ;
take P2 = P2; :: thesis: P2 is_Walk_from u,v
the Path of W1 is_Walk_from u,v by A2, GLIB_001:160;
hence P2 is_Walk_from u,v by GLIB_001:19; :: thesis: verum

end;

suppose ex w, e being object st
( e Joins w,w,G1 & the Path of W1 = G1 .walkOf (w,e,w) ) ; :: thesis: ex W2 being Walk of G2 st b₃ is_Walk_from W2,b₂

then 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; :: thesis: W2 is_Walk_from u,v
thus W2 is_Walk_from u,v by A4, A5, GLIB_001:13; :: thesis: verum

end;

end;

end;

hence G2 is connected by GLIB_002:def 1; :: thesis: verum

end;

assume A6: G2 is connected ; :: thesis: G1 is connected

now :: thesis: for u, v being Vertex of G1 ex W1 being Walk of G1 st W1 is_Walk_from u,v

let u, v be Vertex of G1; :: thesis: ex W1 being Walk of G1 st W1 is_Walk_from u,v
( u is Vertex of G2 & v is Vertex of G2 ) by Th15;
then consider W2 being Walk of G2 such that
A7: W2 is_Walk_from u,v by A6, GLIB_002:def 1;
G2 is Subgraph of G1 by GLIB_006:57;
then reconsider W1 = W2 as Walk of G1 by GLIB_001:167;
take W1 = W1; :: thesis: W1 is_Walk_from u,v
thus W1 is_Walk_from u,v by A7, GLIB_001:19; :: thesis: verum

end;

hence G1 is connected by GLIB_002:def 1; :: thesis: verum