let G be _Graph; ( G is acyclic implies G is simple )
assume A1:
for W being Walk of G holds not W is Cycle-like
; GLIB_002:def 2 G is simple
now 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
;
contradictionset 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;
verum end;
then A4:
G is loopless
by GLIB_000:def 18;
now for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2let e1,
e2,
v1,
v2 be
object ;
( 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
;
e1 = e2A7:
e2 Joins v2,
v1,
G
by A6, GLIB_000:14;
A8:
v1 <> v2
by A4, A5, GLIB_000:18;
now ( 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
;
( (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;
(
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;
contradictionthen
(G .walkOf (v1,e1,v2)) .addEdge e2 is
Cycle-like
by A18, A20, GLIB_001:def 31;
hence
contradiction
by A1;
verum end; hence
e1 = e2
;
verum end;
then
G is non-multi
by GLIB_000:def 20;
hence
G is simple
by A4; verum