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
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 )
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 G .walkOf (v1,e,v1) is V5() 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;
then A4: G is loopless by GLIB_000:def 18;
now :: thesis: for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
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;
now :: thesis: ( e1 <> e2 implies ( (G .walkOf (v1,e1,v2)) .addEdge e2 is Path-like & contradiction ) )
set 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;
A13: now :: thesis: for n being odd Element of NAT st 1 < n & n <= len W1 holds
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;
( W1 .first() = v1 & W1 .last() = v2 ) by A5, GLIB_001:15;
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: (G .walkOf (v1,e1,v2)) .addEdge e2 is V5() 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;
hence e1 = e2 ; :: thesis: verum
end;
then G is non-multi by GLIB_000:def 20;
hence G is simple by A4; :: thesis: verum