let G2 be LGraphComplement 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 Joins w1,w2,G

proof

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

end;

then consider e being object such that
A3: e Joins w1,w2,G2 by Def7;

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 Def7;

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

suppose A4: ( ex e1 being object st e1 Joins v1,w1,G & ex e2 being object st e2 Joins 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 Joins v1,w1,G ;
consider e2 being object such that
A6: e2 Joins v2,w2,G by A4;
for e3 being object holds not e3 Joins u1,w2,G

proof

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

end;

then consider e3 being object such that
A9: e3 Joins u1,w2,G2 by Def7;
for e4 being object holds not e4 Joins w1,u2,G

proof

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

end;

then consider e4 being object such that
A12: e4 Joins w1,u2,G2 by Def7;
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
A13: G2 .walkOf (v1,e3,w2) is_Walk_from v1,w2 by A9, GLIB_001:15;
e Joins w2,w1,G2 by A3, GLIB_000:14;
then G2 .walkOf (w2,e,w1) is_Walk_from w2,w1 by GLIB_001:15;
then A14: (G2 .walkOf (v1,e3,w2)) .append (G2 .walkOf (w2,e,w1)) is_Walk_from v1,w1 by A13, GLIB_001:31;
G2 .walkOf (w1,e4,v2) is_Walk_from w1,v2 by A12, GLIB_001:15;
hence W is_Walk_from v1,v2 by A14, GLIB_001:31; :: thesis: verum

end;

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

then consider e2 being object such that
A16: e2 Joins v2,w2,G ;
consider e3 being object such that
A17: e3 Joins u1,w1,G2 by A15, Def7;
for e4 being object holds not e4 Joins w1,u2,G

proof

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

end;

then consider e4 being object such that
A20: e4 Joins w1,u2,G2 by Def7;
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
A21: G2 .walkOf (v1,e3,w1) is_Walk_from v1,w1 by A17, GLIB_001:15;
G2 .walkOf (w1,e4,v2) is_Walk_from w1,v2 by A20, GLIB_001:15;
hence W is_Walk_from v1,v2 by A21, GLIB_001:31; :: thesis: verum

end;

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

then consider e1 being object such that
A23: e1 Joins v1,w1,G ;
for e3 being object holds not e3 Joins u1,w2,G

proof

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

end;

then consider e3 being object such that
A26: e3 Joins u1,w2,G2 by Def7;
consider e4 being object such that
A27: e4 Joins u2,w2,G2 by A22, Def7;
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
A28: G2 .walkOf (v1,e3,w2) is_Walk_from v1,w2 by A26, GLIB_001:15;
e4 Joins w2,v2,G2 by A27, GLIB_000:14;
then G2 .walkOf (w2,e4,v2) is_Walk_from w2,v2 by GLIB_001:15;
hence W is_Walk_from v1,v2 by A28, GLIB_001:31; :: thesis: verum

end;

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

then consider e3 being object such that
A30: e3 Joins u1,w1,G2 by Def7;
consider e4 being object such that
A31: e4 Joins u2,w2,G2 by A29, Def7;
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
A32: G2 .walkOf (v1,e3,w1) is_Walk_from v1,w1 by A30, GLIB_001:15;
G2 .walkOf (w1,e,w2) is_Walk_from w1,w2 by A3, GLIB_001:15;
then A33: (G2 .walkOf (v1,e3,w1)) .append (G2 .walkOf (w1,e,w2)) is_Walk_from v1,w2 by A32, GLIB_001:31;
e4 Joins w2,v2,G2 by A31, GLIB_000:14;
then G2 .walkOf (w2,e4,v2) is_Walk_from w2,v2 by GLIB_001:15;
hence W is_Walk_from v1,v2 by A33, GLIB_001:31; :: thesis: verum

end;

end;

end;

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