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 () . e = () . e )
given e being object such that A2: e in the_Edges_of G and
A3: (the_Source_of G) . e = () . e ; :: thesis: contradiction
set v1 = () . e;
reconsider v1 = () . e as Vertex of G by ;
set W = G .walkOf (v1,e,v1);
e Joins v1,v1,G by ;
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;
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 ;
A8: v1 <> v2 by ;
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 ;
then A11: ((G .walkOf (v1,e1,v2)) .addEdge e2) .last() = v1 by ;
A12: len W1 = 3 by ;
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 ;
then 2 * 1 < n by XXREAL_0:1;
then (2 * 1) + 1 <= n by NAT_1:13;
then A16: n = 3 by ;
W1 = <*v1,e1,v2*> by ;
hence W1 . n <> v1 by ; :: thesis: verum
end;
( W1 .first() = v1 & W1 .last() = v2 ) by ;
then A17: W1 is open by ;
W1 .first() = v1 by ;
then ((G .walkOf (v1,e1,v2)) .addEdge e2) .first() = v1 by ;
then A18: (G .walkOf (v1,e1,v2)) .addEdge e2 is closed by ;
A19: e2 Joins W1 .last() ,v1,G by ;
then A20: not (G .walkOf (v1,e1,v2)) .addEdge e2 is trivial by GLIB_001:132;
W1 .edges() = {e1} by ;
then not e2 in W1 .edges() by ;
hence (G .walkOf (v1,e1,v2)) .addEdge e2 is Path-like by ; :: thesis: contradiction
then (G .walkOf (v1,e1,v2)) .addEdge e2 is Cycle-like by ;
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