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 A1, Th75;

hence ( G1 is acyclic iff G2 is acyclic ) by A1, Th139; :: 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 ;

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

( ( 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 A1, Th75;

hence ( G1 is acyclic iff G2 is acyclic ) by A1, Th139; :: 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

end;now :: thesis: for P being Walk of G2 st P .length() > 3 & P is Cycle-like holds

P is chordal

hence
G2 is chordal
by CHORD:def 11; :: thesis: verumP 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

end;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 ) )

hence
P is chordal
by CHORD:def 10; :: thesis: verum( 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 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: 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 A7, Th125; :: 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 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: ( 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 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: for f being object st f in P .edges() holds

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 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: verum

end;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: 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 A7, Th125; :: 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 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: ( 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 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: for f being object st f in P .edges() holds

not f Joins P . m,P . n,G2

proof

let f be object ; :: thesis: ( f in P .edges() implies not f Joins P . m,P . n,G2 )
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: 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;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: 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

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 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: verum

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

assume A22:
G2 is chordal
; :: thesis: G1 is chordal

end;now :: thesis: for P being Walk of G1 st P .length() > 3 & P is Cycle-like holds

P is chordal

hence
G1 is chordal
by CHORD:def 11; :: thesis: verumP 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

end;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 ) )

hence
P is chordal
by CHORD:def 10; :: thesis: verum( 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 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: 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 A25, Th125; :: 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 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: ( 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 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: for f being object st f in P .edges() holds

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 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: verum

end;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: 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 A25, Th125; :: 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 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: ( 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 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: for f being object st f in P .edges() holds

not f Joins P . m,P . n,G1

proof

let f be object ; :: thesis: ( f in P .edges() implies not f Joins P . m,P . n,G1 )
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: 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;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: 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

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 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: verum

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

assume A43:
G2 is connected
; :: thesis: 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

end;for u, v being Vertex of G2 ex W2 being Walk of G2 st W2 is_Walk_from u,v

proof

hence
G2 is connected
by GLIB_002:def 1; :: thesis: verum
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 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 .: 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 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: verum

end;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 .: 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 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: verum

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

proof

hence
G1 is connected
by GLIB_002:def 1; :: thesis: verum
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 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: 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 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: verum

end;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: 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 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: verum