let G1 be addAdjVertex of G,v1,e,v2; G1 is acyclic
per cases
( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ) )
;
suppose A1:
(
v1 in the_Vertices_of G & not
v2 in the_Vertices_of G & not
e in the_Edges_of G )
;
G1 is acyclic consider G3 being
addVertex of
G,
v2 such that A2:
G1 is
addEdge of
G3,
v1,
e,
v2
by A1, Th129;
reconsider w1 =
v1 as
Vertex of
G3 by A1, Th72;
A3:
v2 in {v2}
by TARSKI:def 1;
reconsider w2 =
v2 as
Vertex of
G3 by Th98;
w2 in {v2} \ (the_Vertices_of G)
by A3, A1, XBOOLE_0:def 5;
then
w2 is
isolated
by Th92;
then
not
w1 in G3 .reachableFrom w2
by A1, Th53;
then
not
w2 in G3 .reachableFrom w1
by Th54;
hence
G1 is
acyclic
by A2, Th122;
verum end; suppose A6:
( not
v1 in the_Vertices_of G &
v2 in the_Vertices_of G & not
e in the_Edges_of G )
;
G1 is acyclic consider G3 being
addVertex of
G,
v1 such that A7:
G1 is
addEdge of
G3,
v1,
e,
v2
by A6, Th130;
reconsider w2 =
v2 as
Vertex of
G3 by A6, Th72;
A8:
v1 in {v1}
by TARSKI:def 1;
reconsider w1 =
v1 as
Vertex of
G3 by Th98;
w1 in {v1} \ (the_Vertices_of G)
by A8, A6, XBOOLE_0:def 5;
then A9:
w1 is
isolated
by Th92;
not
w2 in G3 .reachableFrom w1
by A6, A9, Th53;
hence
G1 is
acyclic
by A7, Th122;
verum end;