let G1, G2 be _Graph; :: thesis:
let F be PGraphMapping of G1,G2; :: thesis:
assume A1: F is isomorphism ; :: thesis:
then reconsider F = F as non empty one-to-one PGraphMapping of G1,G2 ;
A2: ( F " is isomorphism & F " is semi-continuous ) by A1, Th75;
hence ( G1 is acyclic iff G2 is acyclic ) by A1, Th139; :: thesis:
A3: F is semi-continuous ;

hereby :: thesis:

assume A4: G1 is chordal ; :: thesis:

let P be Walk of G2; :: thesis:
assume A5: ( P .length() > 3 & P is Cycle-like ) ; :: thesis:

reconsider C = P as F -valued Walk of G2 by A1, Th122;
A6: (F " C) .length() > 3 by A5, Th125;
F " C is Cycle-like by A5, Th138;
then F " C is chordal by A4, A6, CHORD:def 11;
then consider m, n being odd Nat such that
A7: ( m + 2 < n & n <= len (F " C) & (F " C) . m <> (F " C) . n ) and
A8: ex e being object st e Joins (F " C) . m,(F " C) . n,G1 and
A9: for f being object st f in (F " C) .edges() holds
not f Joins (F " C) . m,(F " C) . n,G1 by CHORD:def 10;
take m = m; :: thesis:
take n = n; :: thesis:
thus A10: ( m + 2 < n & n <= len P ) by A7, Th125; :: thesis:
A11: n is odd Element of NAT by ORDINAL1:def 12;
then A12: (F " C) . n = ((F ") _V) . (C . n) by A10, Th129;
(m + 2) - 2 <= n - 0 by A10, XREAL_1:13;
then A13: m <= len P by A10, XXREAL_0:2;
A14: m is odd Element of NAT by ORDINAL1:def 12;
then A15: (F " C) . m = ((F ") _V) . (C . m) by A13, Th129;
hence P . m <> P . n by A7, A12; :: thesis:
( P . m in the_Vertices_of G2 & P . n in the_Vertices_of G2 ) by A10, A11, A13, A14, GLIB_001:7;
then A16: ( P . m in dom ((F ") _V) & P . n in dom ((F ") _V) ) by A2, Def11;
thus ex e being object st e Joins P . m,P . n,G2 :: thesis:

consider e0 being object such that
A17: e0 Joins (F " C) . m,(F " C) . n,G1 by A8;
e0 in the_Edges_of G1 by A17, GLIB_000:def 13;
then e0 in rng ((F ") _E) by A2, Def12;
then consider e being object such that
A18: ( e in dom ((F ") _E) & ((F ") _E) . e = e0 ) by FUNCT_1:def 3;
take e ; :: thesis:
((F ") _E) . e Joins ((F ") _V) . (C . m),((F ") _V) . (C . n),G1 by A12, A15, A17, A18;
hence e Joins P . m,P . n,G2 by A2, A16, A18; :: thesis:

end;

let f be object ; :: thesis:
assume A19: f in P .edges() ; :: thesis:
then f in the_Edges_of G2 ;
then A20: f in dom ((F ") _E) by A2, Def11;
then ((F ") _E) . f in ((F ") _E) .: (P .edges()) by A19, FUNCT_1:def 6;
then A21: ((F ") _E) . f in (F " C) .edges() by Th136;
thus not f Joins P . m,P . n,G2 by A9, A12, A15, A16, A20, A21, Th4; :: thesis:

end;

hence P is chordal by CHORD:def 10; :: thesis:

end;

hence G2 is chordal by CHORD:def 11; :: thesis:

end;

hereby :: thesis:

assume A22: G2 is chordal ; :: thesis:

let P be Walk of G1; :: thesis:
assume A23: ( P .length() > 3 & P is Cycle-like ) ; :: thesis:

reconsider C = P as F -defined Walk of G1 by A1, Th121;
A24: (F .: C) .length() > 3 by A23, Th125;
F .: C is Cycle-like by A23, Th138;
then F .: C is chordal by A22, A24, CHORD:def 11;
then consider m, n being odd Nat such that
A25: ( m + 2 < n & n <= len (F .: C) & (F .: C) . m <> (F .: C) . n ) and
A26: ex e being object st e Joins (F .: C) . m,(F .: C) . n,G2 and
A27: for f being object st f in (F .: C) .edges() holds
not f Joins (F .: C) . m,(F .: C) . n,G2 by CHORD:def 10;
take m = m; :: thesis:
take n = n; :: thesis:
thus A28: ( m + 2 < n & n <= len P ) by A25, Th125; :: thesis:
A29: n is odd Element of NAT by ORDINAL1:def 12;
then A30: (F .: C) . n = (F _V) . (C . n) by A28, Th129;
(m + 2) - 2 <= n - 0 by A28, XREAL_1:13;
then A31: m <= len P by A28, XXREAL_0:2;
A32: m is odd Element of NAT by ORDINAL1:def 12;
then A33: (F .: C) . m = (F _V) . (C . m) by A31, Th129;
hence P . m <> P . n by A25, A30; :: thesis:
( P . m in the_Vertices_of G1 & P . n in the_Vertices_of G1 ) by A28, A29, A31, A32, GLIB_001:7;
then A34: ( P . m in dom (F _V) & P . n in dom (F _V) ) by A1, Def11;
thus ex e being object st e Joins P . m,P . n,G1 :: thesis:

consider e0 being object such that
A35: e0 Joins (F .: C) . m,(F .: C) . n,G2 by A26;
e0 in the_Edges_of G2 by A35, GLIB_000:def 13;
then e0 in rng (F _E) by A1, Def12;
then consider e being object such that
A36: ( e in dom (F _E) & (F _E) . e = e0 ) by FUNCT_1:def 3;
take e ; :: thesis:
(F _E) . e Joins (F _V) . (C . m),(F _V) . (C . n),G2 by A30, A33, A35, A36;
hence e Joins P . m,P . n,G1 by A3, A34, A36; :: thesis:

end;

let f be object ; :: thesis:
assume A37: f in P .edges() ; :: thesis:
then f in the_Edges_of G1 ;
then A38: f in dom (F _E) by A1, Def11;
then (F _E) . f in (F _E) .: (P .edges()) by A37, FUNCT_1:def 6;
then A39: (F _E) . f in (F .: C) .edges() by Th136;
thus not f Joins P . m,P . n,G1 by A27, A30, A33, A34, A38, A39, Th4; :: thesis:

end;

hence P is chordal by CHORD:def 10; :: thesis:

end;

hence G1 is chordal by CHORD:def 11; :: thesis:

end;

hereby :: thesis:

assume A40: G1 is connected ; :: thesis:
for u, v being Vertex of G2 ex W2 being Walk of G2 st W2 is_Walk_from u,v

let u2, v2 be Vertex of G2; :: thesis:
reconsider u1 = ((F ") _V) . u2, v1 = ((F ") _V) . v2 as Vertex of G1 by A1, Th79;
consider W1 being Walk of G1 such that
A41: W1 is_Walk_from u1,v1 by A40, GLIB_002:def 1;
reconsider W1 = W1 as F -defined Walk of G1 by A1, Th121;
take F .: W1 ; :: thesis:
F " is total by A2;
then ( u2 in dom ((F _V) ") & v2 in dom ((F _V) ") ) ;
then A42: ( u2 in rng (F _V) & v2 in rng (F _V) ) by FUNCT_1:33;
F .: W1 is_Walk_from (F _V) . (((F _V) ") . u2),(F _V) . v1 by A41, Th132;
then F .: W1 is_Walk_from u2,(F _V) . (((F _V) ") . v2) by A42, FUNCT_1:35;
hence F .: W1 is_Walk_from u2,v2 by A42, FUNCT_1:35; :: thesis:

end;

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

end;

assume A43: G2 is connected ; :: thesis:
for u, v being Vertex of G1 ex W1 being Walk of G1 st W1 is_Walk_from u,v

let u1, v1 be Vertex of G1; :: thesis:
reconsider u2 = (F _V) . u1, v2 = (F _V) . v1 as Vertex of G2 by A1, Th34;
consider W2 being Walk of G2 such that
A44: W2 is_Walk_from u2,v2 by A43, GLIB_002:def 1;
reconsider W2 = W2 as F -valued Walk of G2 by A1, Th122;
take F " W2 ; :: thesis:
A45: F is total by A1;
F " W2 is_Walk_from ((F _V) ") . ((F _V) . u1),((F ") _V) . v2 by A44, Th132;
then F " W2 is_Walk_from u1,((F _V) ") . ((F _V) . v1) by A45, FUNCT_1:34;
hence F " W2 is_Walk_from u1,v1 by A45, FUNCT_1:34; :: thesis:

end;

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