let G2 be DLGraphComplement of G; :: thesis: G2 is connected
consider w1, w2 being Vertex of G such that
A1: for W being Walk of G holds not W is_Walk_from w1,w2 by GLIB_002:def 1;
for e being object holds not e DJoins w1,w2,G

proof

given e being object such that A2: e DJoins w1,w2,G ; :: thesis: contradiction
e Joins w1,w2,G by A2, GLIB_000:16;
then G .walkOf (w1,e,w2) is_Walk_from w1,w2 by GLIB_001:15;
hence contradiction by A1; :: thesis: verum

end;

then consider e being object such that
A3: e DJoins w1,w2,G2 by Def6;

now :: thesis: for v1, v2 being Vertex of G2 ex W being Walk of G2 st W is_Walk_from v1,v2

let v1, v2 be Vertex of G2; :: thesis: ex W being Walk of G2 st b₃ is_Walk_from W,b₂
reconsider u1 = v1, u2 = v2 as Vertex of G by Def6;

per cases ( ( ex e1 being object st e1 DJoins v1,w1,G & ex e2 being object st e2 DJoins v2,w2,G ) or ( ( for e1 being object holds not e1 DJoins v1,w1,G ) & ex e2 being object st e2 DJoins v2,w2,G ) or ( ex e1 being object st e1 DJoins v1,w1,G & ( for e2 being object holds not e2 DJoins v2,w2,G ) ) or ( ( for e1 being object holds not e1 DJoins v1,w1,G ) & ( for e2 being object holds not e2 DJoins v2,w2,G ) ) ) ;

suppose A4: ( ex e1 being object st e1 DJoins v1,w1,G & ex e2 being object st e2 DJoins v2,w2,G ) ; :: thesis: ex W being Walk of G2 st b₃ is_Walk_from W,b₂

then consider e1 being object such that
A5: e1 DJoins v1,w1,G ;
consider e2 being object such that
A6: e2 DJoins v2,w2,G by A4;
A7: e1 Joins w1,v1,G by A5, GLIB_000:16;
A8: e2 Joins v2,w2,G by A6, GLIB_000:16;
for e3 being object holds not e3 DJoins u1,w2,G

proof

given e3 being object such that A9: e3 DJoins u1,w2,G ; :: thesis: contradiction
set W2 = G .walkOf (v1,e3,w2);
e3 Joins v1,w2,G by A9, GLIB_000:16;
then A10: G .walkOf (v1,e3,w2) is_Walk_from v1,w2 by GLIB_001:15;
set W1 = G .walkOf (w1,e1,v1);
G .walkOf (w1,e1,v1) is_Walk_from w1,v1 by A7, GLIB_001:15;
then (G .walkOf (w1,e1,v1)) .append (G .walkOf (v1,e3,w2)) is_Walk_from w1,w2 by A10, GLIB_001:31;
hence contradiction by A1; :: thesis: verum

end;

then consider e3 being object such that
A11: e3 DJoins u1,w2,G2 by Def6;
A12: e3 Joins v1,w2,G2 by A11, GLIB_000:16;
for e4 being object holds not e4 DJoins w1,u2,G

proof

given e4 being object such that A13: e4 DJoins w1,u2,G ; :: thesis: contradiction
set W1 = G .walkOf (w1,e4,u2);
e4 Joins w1,v2,G by A13, GLIB_000:16;
then A14: G .walkOf (w1,e4,u2) is_Walk_from w1,v2 by GLIB_001:15;
set W2 = G .walkOf (v2,e2,w2);
G .walkOf (v2,e2,w2) is_Walk_from v2,w2 by A8, GLIB_001:15;
then (G .walkOf (w1,e4,u2)) .append (G .walkOf (v2,e2,w2)) is_Walk_from w1,w2 by A14, GLIB_001:31;
hence contradiction by A1; :: thesis: verum

end;

then consider e4 being object such that
A15: e4 DJoins w1,u2,G2 by Def6;
A16: e4 Joins w1,v2,G2 by A15, GLIB_000:16;
set W1 = G2 .walkOf (v1,e3,w2);
set W2 = G2 .walkOf (w2,e,w1);
set W3 = G2 .walkOf (w1,e4,v2);
reconsider W = ((G2 .walkOf (v1,e3,w2)) .append (G2 .walkOf (w2,e,w1))) .append (G2 .walkOf (w1,e4,v2)) as Walk of G2 ;
take W = W; :: thesis: W is_Walk_from v1,v2
A17: G2 .walkOf (v1,e3,w2) is_Walk_from v1,w2 by A12, GLIB_001:15;
e Joins w2,w1,G2 by A3, GLIB_000:16;
then G2 .walkOf (w2,e,w1) is_Walk_from w2,w1 by GLIB_001:15;
then A18: (G2 .walkOf (v1,e3,w2)) .append (G2 .walkOf (w2,e,w1)) is_Walk_from v1,w1 by A17, GLIB_001:31;
G2 .walkOf (w1,e4,v2) is_Walk_from w1,v2 by A16, GLIB_001:15;
hence W is_Walk_from v1,v2 by A18, GLIB_001:31; :: thesis: verum

end;

suppose A19: ( ( for e1 being object holds not e1 DJoins v1,w1,G ) & ex e2 being object st e2 DJoins v2,w2,G ) ; :: thesis: ex W being Walk of G2 st b₃ is_Walk_from W,b₂

then consider e2 being object such that
A20: e2 DJoins v2,w2,G ;
A21: e2 Joins v2,w2,G by A20, GLIB_000:16;
consider e3 being object such that
A22: e3 DJoins u1,w1,G2 by A19, Def6;
A23: e3 Joins v1,w1,G2 by A22, GLIB_000:16;
for e4 being object holds not e4 DJoins w1,u2,G

proof

given e4 being object such that A24: e4 DJoins w1,u2,G ; :: thesis: contradiction
set W1 = G .walkOf (w1,e4,u2);
e4 Joins w1,v2,G by A24, GLIB_000:16;
then A25: G .walkOf (w1,e4,u2) is_Walk_from w1,v2 by GLIB_001:15;
set W2 = G .walkOf (v2,e2,w2);
G .walkOf (v2,e2,w2) is_Walk_from v2,w2 by A21, GLIB_001:15;
then (G .walkOf (w1,e4,u2)) .append (G .walkOf (v2,e2,w2)) is_Walk_from w1,w2 by A25, GLIB_001:31;
hence contradiction by A1; :: thesis: verum

end;

then consider e4 being object such that
A26: e4 DJoins w1,u2,G2 by Def6;
A27: e4 Joins w1,v2,G2 by A26, GLIB_000:16;
set W1 = G2 .walkOf (v1,e3,w1);
set W2 = G2 .walkOf (w1,e4,v2);
reconsider W = (G2 .walkOf (v1,e3,w1)) .append (G2 .walkOf (w1,e4,v2)) as Walk of G2 ;
take W = W; :: thesis: W is_Walk_from v1,v2
A28: G2 .walkOf (v1,e3,w1) is_Walk_from v1,w1 by A23, GLIB_001:15;
G2 .walkOf (w1,e4,v2) is_Walk_from w1,v2 by A27, GLIB_001:15;
hence W is_Walk_from v1,v2 by A28, GLIB_001:31; :: thesis: verum

end;

suppose A29: ( ex e1 being object st e1 DJoins v1,w1,G & ( for e2 being object holds not e2 DJoins v2,w2,G ) ) ; :: thesis: ex W being Walk of G2 st b₃ is_Walk_from W,b₂

then consider e1 being object such that
A30: e1 DJoins v1,w1,G ;
A31: e1 Joins w1,v1,G by A30, GLIB_000:16;
for e3 being object holds not e3 DJoins u1,w2,G

proof

given e3 being object such that A32: e3 DJoins u1,w2,G ; :: thesis: contradiction
set W2 = G .walkOf (v1,e3,w2);
e3 Joins v1,w2,G by A32, GLIB_000:16;
then A33: G .walkOf (v1,e3,w2) is_Walk_from v1,w2 by GLIB_001:15;
set W1 = G .walkOf (w1,e1,v1);
G .walkOf (w1,e1,v1) is_Walk_from w1,v1 by A31, GLIB_001:15;
then (G .walkOf (w1,e1,v1)) .append (G .walkOf (v1,e3,w2)) is_Walk_from w1,w2 by A33, GLIB_001:31;
hence contradiction by A1; :: thesis: verum

end;

then consider e3 being object such that
A34: e3 DJoins u1,w2,G2 by Def6;
A35: e3 Joins v1,w2,G2 by A34, GLIB_000:16;
consider e4 being object such that
A36: e4 DJoins u2,w2,G2 by A29, Def6;
A37: e4 Joins w2,v2,G2 by A36, GLIB_000:16;
set W1 = G2 .walkOf (v1,e3,w2);
set W2 = G2 .walkOf (w2,e4,v2);
reconsider W = (G2 .walkOf (v1,e3,w2)) .append (G2 .walkOf (w2,e4,v2)) as Walk of G2 ;
take W = W; :: thesis: W is_Walk_from v1,v2
A38: G2 .walkOf (v1,e3,w2) is_Walk_from v1,w2 by A35, GLIB_001:15;
G2 .walkOf (w2,e4,v2) is_Walk_from w2,v2 by A37, GLIB_001:15;
hence W is_Walk_from v1,v2 by A38, GLIB_001:31; :: thesis: verum

end;

suppose A39: ( ( for e1 being object holds not e1 DJoins v1,w1,G ) & ( for e2 being object holds not e2 DJoins v2,w2,G ) ) ; :: thesis: ex W being Walk of G2 st b₃ is_Walk_from W,b₂

then consider e3 being object such that
A40: e3 DJoins u1,w1,G2 by Def6;
A41: e3 Joins v1,w1,G2 by A40, GLIB_000:16;
consider e4 being object such that
A42: e4 DJoins u2,w2,G2 by A39, Def6;
A43: e4 Joins w2,v2,G2 by A42, GLIB_000:16;
set W1 = G2 .walkOf (v1,e3,w1);
set W2 = G2 .walkOf (w1,e,w2);
set W3 = G2 .walkOf (w2,e4,v2);
reconsider W = ((G2 .walkOf (v1,e3,w1)) .append (G2 .walkOf (w1,e,w2))) .append (G2 .walkOf (w2,e4,v2)) as Walk of G2 ;
take W = W; :: thesis: W is_Walk_from v1,v2
A44: G2 .walkOf (v1,e3,w1) is_Walk_from v1,w1 by A41, GLIB_001:15;
e Joins w1,w2,G2 by A3, GLIB_000:16;
then G2 .walkOf (w1,e,w2) is_Walk_from w1,w2 by GLIB_001:15;
then A45: (G2 .walkOf (v1,e3,w1)) .append (G2 .walkOf (w1,e,w2)) is_Walk_from v1,w2 by A44, GLIB_001:31;
G2 .walkOf (w2,e4,v2) is_Walk_from w2,v2 by A43, GLIB_001:15;
hence W is_Walk_from v1,v2 by A45, GLIB_001:31; :: thesis: verum

end;

end;

end;

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