let G2 be _Graph; for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & v2 in G2 .reachableFrom v1 holds
not G1 is acyclic
let v1, v2 be Vertex of G2; for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & v2 in G2 .reachableFrom v1 holds
not G1 is acyclic
let e be object ; for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & v2 in G2 .reachableFrom v1 holds
not G1 is acyclic
let G1 be addEdge of G2,v1,e,v2; ( not e in the_Edges_of G2 & v2 in G2 .reachableFrom v1 implies not G1 is acyclic )
assume that
A1:
not e in the_Edges_of G2
and
A2:
v2 in G2 .reachableFrom v1
; not G1 is acyclic
per cases
( v1 <> v2 or v1 = v2 )
;
suppose A3:
v1 <> v2
;
not G1 is acyclic consider W2 being
Walk of
G2 such that A4:
W2 is_Walk_from v1,
v2
by A2, GLIB_002:def 5;
reconsider W1 =
W2 as
Walk of
G1 by Th79;
set P = the
Path of
W1;
W1 is_Walk_from v1,
v2
by A4, GLIB_001:19;
then
the
Path of
W1 is_Walk_from v1,
v2
by GLIB_001:160;
then A6:
( the
Path of
W1 .first() = v1 & the
Path of
W1 .last() = v2 )
by GLIB_001:def 23;
set W = the
Path of
W1 .addEdge e;
e DJoins v1,
v2,
G1
by A1, Th109;
then A7:
e Joins v2,
v1,
G1
by GLIB_000:16;
then A8:
the
Path of
W1 .addEdge e is
closed
by A6, GLIB_001:63, GLIB_001:119;
A9:
the
Path of
W1 .addEdge e is
trivial
by A6, A7, GLIB_001:132;
not
e in W2 .edges()
by A1;
then
not
e in W1 .edges()
by GLIB_001:110;
then A10:
not
e in the
Path of
W1 .edges()
by GLIB_001:163, TARSKI:def 3;
A11:
the
Path of
W1 is
open
by A3, A6, GLIB_001:def 24;
for
n being
odd Element of
NAT st 1
< n &
n <= len the
Path of
W1 holds
the
Path of
W1 . n <> v1
then
the
Path of
W1 .addEdge e is
Path-like
by A6, A7, A10, A11, GLIB_001:150;
hence
not
G1 is
acyclic
by A8, A9, GLIB_002:def 2;
verum end;