let G be _Graph; :: thesis: ( G is acyclic implies G is simple )

assume A1: for W being Walk of G holds not W is Cycle-like ; :: according to GLIB_002:def 2 :: thesis: G is simple

hence G is simple by A4; :: thesis: verum

assume A1: for W being Walk of G holds not W is Cycle-like ; :: according to GLIB_002:def 2 :: thesis: G is simple

now :: thesis: for e being object holds

( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e )

then A4:
G is loopless
by GLIB_000:def 18;( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e )

given e being object such that A2:
e in the_Edges_of G
and

A3: (the_Source_of G) . e = (the_Target_of G) . e ; :: thesis: contradiction

set v1 = (the_Source_of G) . e;

reconsider v1 = (the_Source_of G) . e as Vertex of G by A2, FUNCT_2:5;

set W = G .walkOf (v1,e,v1);

e Joins v1,v1,G by A2, A3, GLIB_000:def 13;

then len (G .walkOf (v1,e,v1)) = 3 by GLIB_001:14;

then not G .walkOf (v1,e,v1) is trivial by GLIB_001:125;

then G .walkOf (v1,e,v1) is Cycle-like by GLIB_001:def 31;

hence contradiction by A1; :: thesis: verum

end;A3: (the_Source_of G) . e = (the_Target_of G) . e ; :: thesis: contradiction

set v1 = (the_Source_of G) . e;

reconsider v1 = (the_Source_of G) . e as Vertex of G by A2, FUNCT_2:5;

set W = G .walkOf (v1,e,v1);

e Joins v1,v1,G by A2, A3, GLIB_000:def 13;

then len (G .walkOf (v1,e,v1)) = 3 by GLIB_001:14;

then not G .walkOf (v1,e,v1) is trivial by GLIB_001:125;

then G .walkOf (v1,e,v1) is Cycle-like by GLIB_001:def 31;

hence contradiction by A1; :: thesis: verum

now :: thesis: for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds

e1 = e2

then
G is non-multi
by GLIB_000:def 20;e1 = e2

let e1, e2, v1, v2 be object ; :: thesis: ( e1 Joins v1,v2,G & e2 Joins v1,v2,G implies e1 = e2 )

assume that

A5: e1 Joins v1,v2,G and

A6: e2 Joins v1,v2,G ; :: thesis: e1 = e2

A7: e2 Joins v2,v1,G by A6, GLIB_000:14;

A8: v1 <> v2 by A4, A5, GLIB_000:18;

end;assume that

A5: e1 Joins v1,v2,G and

A6: e2 Joins v1,v2,G ; :: thesis: e1 = e2

A7: e2 Joins v2,v1,G by A6, GLIB_000:14;

A8: v1 <> v2 by A4, A5, GLIB_000:18;

now :: thesis: ( e1 <> e2 implies ( (G .walkOf (v1,e1,v2)) .addEdge e2 is Path-like & contradiction ) )

hence
e1 = e2
; :: thesis: verumset W1 = G .walkOf (v1,e1,v2);

set W = (G .walkOf (v1,e1,v2)) .addEdge e2;

assume A9: e1 <> e2 ; :: thesis: ( (G .walkOf (v1,e1,v2)) .addEdge e2 is Path-like & contradiction )

reconsider W1 = G .walkOf (v1,e1,v2) as Path of G ;

A10: W1 .last() = v2 by A5, GLIB_001:15;

then A11: ((G .walkOf (v1,e1,v2)) .addEdge e2) .last() = v1 by A7, GLIB_001:63;

A12: len W1 = 3 by A5, GLIB_001:14;

then A17: W1 is open by A8, GLIB_001:def 24;

W1 .first() = v1 by A5, GLIB_001:15;

then ((G .walkOf (v1,e1,v2)) .addEdge e2) .first() = v1 by A7, A10, GLIB_001:63;

then A18: (G .walkOf (v1,e1,v2)) .addEdge e2 is closed by A11, GLIB_001:def 24;

A19: e2 Joins W1 .last() ,v1,G by A5, A7, GLIB_001:15;

then A20: not (G .walkOf (v1,e1,v2)) .addEdge e2 is trivial by GLIB_001:132;

W1 .edges() = {e1} by A5, GLIB_001:108;

then not e2 in W1 .edges() by A9, TARSKI:def 1;

hence (G .walkOf (v1,e1,v2)) .addEdge e2 is Path-like by A19, A17, A13, GLIB_001:150; :: thesis: contradiction

then (G .walkOf (v1,e1,v2)) .addEdge e2 is Cycle-like by A18, A20, GLIB_001:def 31;

hence contradiction by A1; :: thesis: verum

end;set W = (G .walkOf (v1,e1,v2)) .addEdge e2;

assume A9: e1 <> e2 ; :: thesis: ( (G .walkOf (v1,e1,v2)) .addEdge e2 is Path-like & contradiction )

reconsider W1 = G .walkOf (v1,e1,v2) as Path of G ;

A10: W1 .last() = v2 by A5, GLIB_001:15;

then A11: ((G .walkOf (v1,e1,v2)) .addEdge e2) .last() = v1 by A7, GLIB_001:63;

A12: len W1 = 3 by A5, GLIB_001:14;

A13: now :: thesis: for n being odd Element of NAT st 1 < n & n <= len W1 holds

W1 . n <> v1

( W1 .first() = v1 & W1 .last() = v2 )
by A5, GLIB_001:15;W1 . n <> v1

let n be odd Element of NAT ; :: thesis: ( 1 < n & n <= len W1 implies W1 . n <> v1 )

assume that

A14: 1 < n and

A15: n <= len W1 ; :: thesis: W1 . n <> v1

1 + 1 <= n by A14, NAT_1:13;

then 2 * 1 < n by XXREAL_0:1;

then (2 * 1) + 1 <= n by NAT_1:13;

then A16: n = 3 by A12, A15, XXREAL_0:1;

W1 = <*v1,e1,v2*> by A5, GLIB_001:def 5;

hence W1 . n <> v1 by A8, A16, FINSEQ_1:45; :: thesis: verum

end;assume that

A14: 1 < n and

A15: n <= len W1 ; :: thesis: W1 . n <> v1

1 + 1 <= n by A14, NAT_1:13;

then 2 * 1 < n by XXREAL_0:1;

then (2 * 1) + 1 <= n by NAT_1:13;

then A16: n = 3 by A12, A15, XXREAL_0:1;

W1 = <*v1,e1,v2*> by A5, GLIB_001:def 5;

hence W1 . n <> v1 by A8, A16, FINSEQ_1:45; :: thesis: verum

then A17: W1 is open by A8, GLIB_001:def 24;

W1 .first() = v1 by A5, GLIB_001:15;

then ((G .walkOf (v1,e1,v2)) .addEdge e2) .first() = v1 by A7, A10, GLIB_001:63;

then A18: (G .walkOf (v1,e1,v2)) .addEdge e2 is closed by A11, GLIB_001:def 24;

A19: e2 Joins W1 .last() ,v1,G by A5, A7, GLIB_001:15;

then A20: not (G .walkOf (v1,e1,v2)) .addEdge e2 is trivial by GLIB_001:132;

W1 .edges() = {e1} by A5, GLIB_001:108;

then not e2 in W1 .edges() by A9, TARSKI:def 1;

hence (G .walkOf (v1,e1,v2)) .addEdge e2 is Path-like by A19, A17, A13, GLIB_001:150; :: thesis: contradiction

then (G .walkOf (v1,e1,v2)) .addEdge e2 is Cycle-like by A18, A20, GLIB_001:def 31;

hence contradiction by A1; :: thesis: verum

hence G is simple by A4; :: thesis: verum