let G be connected _Graph; ( ex v1, v2 being Vertex of G ex e being object ex H being addEdge of G,v1,e,v2 st
( not e in the_Edges_of G & ( for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like holds
W1 .edges() = W2 .edges() ) ) implies G is Tree-like )
given v1, v2 being Vertex of G, e being object , H being addEdge of G,v1,e,v2 such that A1:
not e in the_Edges_of G
and
A2:
for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like holds
W1 .edges() = W2 .edges()
; G is Tree-like
G is acyclic
proof
assume
not
G is
acyclic
;
contradiction
then consider W1 being
Walk of
G such that A3:
W1 is
Cycle-like
by GLIB_002:def 2;
reconsider W3 =
W1 as
Walk of
H by GLIB_006:75;
A4:
W3 is
Cycle-like
by A3, GLIB_006:24;
e DJoins v1,
v2,
H
by A1, GLIB_006:105;
then A5:
e Joins v2,
v1,
H
by GLIB_000:16;
not
e in W1 .edges()
by A1;
then A6:
not
e in W3 .edges()
by GLIB_001:110;
per cases
( v1 <> v2 or v1 = v2 )
;
suppose A7:
v1 <> v2
;
contradictionconsider W2 being
Walk of
G such that A8:
W2 is_Walk_from v1,
v2
by GLIB_002:def 1;
set P2 = the
Path-like Subwalk of
W2;
reconsider P4 = the
Path-like Subwalk of
W2 as
Walk of
H by GLIB_006:75;
set W4 =
P4 .addEdge e;
the
Path-like Subwalk of
W2 is_Walk_from v1,
v2
by A8, GLIB_001:160;
then
P4 is_Walk_from v1,
v2
by GLIB_001:19;
then A9:
(
P4 is
Path-like &
P4 is_Walk_from v1,
v2 )
by GLIB_006:23;
then A10:
P4 .addEdge e is
closed
by A5, GLIB_001:66, GLIB_001:119;
A11:
(
P4 .first() = v1 &
P4 .last() = v2 )
by A9, GLIB_001:def 23;
then A12:
P4 .addEdge e is
V5()
by A5, GLIB_001:132;
A13:
P4 is
open
by A7, A11, GLIB_001:def 24;
not
e in the
Path-like Subwalk of
W2 .edges()
by A1;
then A14:
not
e in P4 .edges()
by GLIB_001:110;
for
n being
odd Element of
NAT st 1
< n &
n <= len P4 holds
P4 . n <> v1
then A16:
P4 .addEdge e is
Path-like
by A5, A9, A11, A13, A14, GLIB_001:150;
e in {e}
by TARSKI:def 1;
then
e in (P4 .edges()) \/ {e}
by XBOOLE_0:def 3;
then
e in (P4 .addEdge e) .edges()
by A5, A11, GLIB_001:111;
hence
contradiction
by A2, A4, A6, A10, A12, A16;
verum end; suppose A17:
v1 = v2
;
contradictionset W4 =
H .walkOf (
v2,
e,
v1);
(H .walkOf (v2,e,v1)) .edges() = {e}
by A5, GLIB_001:108;
then A18:
e in (H .walkOf (v2,e,v1)) .edges()
by TARSKI:def 1;
H .walkOf (
v2,
e,
v1) is
Cycle-like
by A5, A17, GLIB_001:156;
hence
contradiction
by A2, A4, A6, A18;
verum end;
end;
hence
G is Tree-like
; verum