let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
( ( G1 is acyclic implies G2 is acyclic ) & ( G2 is acyclic implies G1 is acyclic ) & ( G1 is chordal implies G2 is chordal ) & ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) )

let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies ( ( G1 is acyclic implies G2 is acyclic ) & ( G2 is acyclic implies G1 is acyclic ) & ( G1 is chordal implies G2 is chordal ) & ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) ) )
assume A1: F is isomorphism ; :: thesis: ( ( G1 is acyclic implies G2 is acyclic ) & ( G2 is acyclic implies G1 is acyclic ) & ( G1 is chordal implies G2 is chordal ) & ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) )
then reconsider F = F as non empty one-to-one PGraphMapping of G1,G2 ;
A2: ( F " is isomorphism & F " is semi-continuous ) by ;
hence ( G1 is acyclic iff G2 is acyclic ) by ; :: thesis: ( ( G1 is chordal implies G2 is chordal ) & ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) )
A3: F is semi-continuous ;
hereby :: thesis: ( ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) )
assume A4: G1 is chordal ; :: thesis: G2 is chordal
now :: thesis: for P being Walk of G2 st P .length() > 3 & P is Cycle-like holds
P is chordal
let P be Walk of G2; :: thesis: ( P .length() > 3 & P is Cycle-like implies P is chordal )
assume A5: ( P .length() > 3 & P is Cycle-like ) ; :: thesis: P is chordal
now :: thesis: ex m, n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G2 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2 ) )
reconsider C = P as F -valued Walk of G2 by ;
A6: (F " C) .length() > 3 by ;
F " C is Cycle-like by ;
then F " C is chordal by ;
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: ex n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G2 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2 ) )

take n = n; :: thesis: ( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G2 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2 ) )

thus A10: ( m + 2 < n & n <= len P ) by ; :: thesis: ( P . m <> P . n & ex e being object st e Joins P . m,P . n,G2 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2 ) )

A11: n is odd Element of NAT by ORDINAL1:def 12;
then A12: (F " C) . n = ((F ") _V) . (C . n) by ;
(m + 2) - 2 <= n - 0 by ;
then A13: m <= len P by ;
A14: m is odd Element of NAT by ORDINAL1:def 12;
then A15: (F " C) . m = ((F ") _V) . (C . m) by ;
hence P . m <> P . n by ; :: thesis: ( ex e being object st e Joins P . m,P . n,G2 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2 ) )

( P . m in the_Vertices_of G2 & P . n in the_Vertices_of G2 ) by ;
then A16: ( P . m in dom ((F ") _V) & P . n in dom ((F ") _V) ) by ;
thus ex e being object st e Joins P . m,P . n,G2 :: thesis: for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2
proof
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 ;
then e0 in rng ((F ") _E) by ;
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: e Joins P . m,P . n,G2
((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: verum
end;
let f be object ; :: thesis: ( f in P .edges() implies not f Joins P . m,P . n,G2 )
assume A19: f in P .edges() ; :: thesis: not f Joins P . m,P . n,G2
then f in the_Edges_of G2 ;
then A20: f in dom ((F ") _E) by ;
then ((F ") _E) . f in ((F ") _E) .: () by ;
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: verum
end;
hence P is chordal by CHORD:def 10; :: thesis: verum
end;
hence G2 is chordal by CHORD:def 11; :: thesis: verum
end;
hereby :: thesis: ( G1 is connected iff G2 is connected )
assume A22: G2 is chordal ; :: thesis: G1 is chordal
now :: thesis: for P being Walk of G1 st P .length() > 3 & P is Cycle-like holds
P is chordal
let P be Walk of G1; :: thesis: ( P .length() > 3 & P is Cycle-like implies P is chordal )
assume A23: ( P .length() > 3 & P is Cycle-like ) ; :: thesis: P is chordal
now :: thesis: ex m, n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )
reconsider C = P as F -defined Walk of G1 by ;
A24: (F .: C) .length() > 3 by ;
F .: C is Cycle-like by ;
then F .: C is chordal by ;
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: ex n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )

take n = n; :: thesis: ( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )

thus A28: ( m + 2 < n & n <= len P ) by ; :: thesis: ( P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )

A29: n is odd Element of NAT by ORDINAL1:def 12;
then A30: (F .: C) . n = (F _V) . (C . n) by ;
(m + 2) - 2 <= n - 0 by ;
then A31: m <= len P by ;
A32: m is odd Element of NAT by ORDINAL1:def 12;
then A33: (F .: C) . m = (F _V) . (C . m) by ;
hence P . m <> P . n by ; :: thesis: ( ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )

( P . m in the_Vertices_of G1 & P . n in the_Vertices_of G1 ) by ;
then A34: ( P . m in dom (F _V) & P . n in dom (F _V) ) by ;
thus ex e being object st e Joins P . m,P . n,G1 :: thesis: for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1
proof
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 ;
then e0 in rng (F _E) by ;
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: e Joins P . m,P . n,G1
(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: verum
end;
let f be object ; :: thesis: ( f in P .edges() implies not f Joins P . m,P . n,G1 )
assume A37: f in P .edges() ; :: thesis: not f Joins P . m,P . n,G1
then f in the_Edges_of G1 ;
then A38: f in dom (F _E) by ;
then (F _E) . f in (F _E) .: () by ;
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: verum
end;
hence P is chordal by CHORD:def 10; :: thesis: verum
end;
hence G1 is chordal by CHORD:def 11; :: thesis: verum
end;
hereby :: thesis: ( G2 is connected implies G1 is connected )
assume A40: G1 is connected ; :: thesis: G2 is connected
for u, v being Vertex of G2 ex W2 being Walk of G2 st W2 is_Walk_from u,v
proof
let u2, v2 be Vertex of G2; :: thesis: ex W2 being Walk of G2 st W2 is_Walk_from u2,v2
reconsider u1 = ((F ") _V) . u2, v1 = ((F ") _V) . v2 as Vertex of G1 by ;
consider W1 being Walk of G1 such that
A41: W1 is_Walk_from u1,v1 by ;
reconsider W1 = W1 as F -defined Walk of G1 by ;
take F .: W1 ; :: thesis: F .: W1 is_Walk_from u2,v2
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 ;
then F .: W1 is_Walk_from u2,(F _V) . (((F _V) ") . v2) by ;
hence F .: W1 is_Walk_from u2,v2 by ; :: thesis: verum
end;
hence G2 is connected by GLIB_002:def 1; :: thesis: verum
end;
assume A43: G2 is connected ; :: thesis: G1 is connected
for u, v being Vertex of G1 ex W1 being Walk of G1 st W1 is_Walk_from u,v
proof
let u1, v1 be Vertex of G1; :: thesis: ex W1 being Walk of G1 st W1 is_Walk_from u1,v1
reconsider u2 = (F _V) . u1, v2 = (F _V) . v1 as Vertex of G2 by ;
consider W2 being Walk of G2 such that
A44: W2 is_Walk_from u2,v2 by ;
reconsider W2 = W2 as F -valued Walk of G2 by ;
take F " W2 ; :: thesis: F " W2 is_Walk_from u1,v1
A45: F is total by A1;
F " W2 is_Walk_from ((F _V) ") . ((F _V) . u1),((F ") _V) . v2 by ;
then F " W2 is_Walk_from u1,((F _V) ") . ((F _V) . v1) by ;
hence F " W2 is_Walk_from u1,v1 by ; :: thesis: verum
end;
hence G1 is connected by GLIB_002:def 1; :: thesis: verum