let G be non edgeless _Graph; :: thesis: for e being Edge of G holds
( createGraph e is acyclic iff not e in G .loops() )
let e be Edge of G; :: thesis: ( createGraph e is acyclic iff not e in G .loops() )
thus ( createGraph e is acyclic implies not e in G .loops() ) by Th17; :: thesis: ( not e in G .loops() implies createGraph e is acyclic )
assume A1: not e in G .loops() ; :: thesis: createGraph e is acyclic
assume not createGraph e is acyclic ; :: thesis: contradiction
then consider W2 being Walk of createGraph e such that
A2: W2 is Cycle-like by GLIB_002:def 2;
A3: len (W2 .vertexSeq()) <= ((createGraph e) .order()) + 1 by A2, GLIB_001:154;
set v = (the_Source_of G) . e;
set w = (the_Target_of G) . e;
A4: the_Vertices_of (createGraph e) = {((the_Source_of G) . e),((the_Target_of G) . e)} by Th13;
card {((the_Source_of G) . e),((the_Target_of G) . e)} <= 2 by CARD_2:50;
then (createGraph e) .order() <= 2 by A4, GLIB_000:def 24;
then ((createGraph e) .order()) + 1 <= 2 + 1 by XREAL_1:6;
then len (W2 .vertexSeq()) <= 2 + 1 by A3, XXREAL_0:2;
then not not len (W2 .vertexSeq()) = 0 & ... & not len (W2 .vertexSeq()) = 3 ;

per cases then ( len (W2 .vertexSeq()) = 0 or len (W2 .vertexSeq()) = 1 or len (W2 .vertexSeq()) = 2 or len (W2 .vertexSeq()) = 3 ) ;

suppose len (W2 .vertexSeq()) = 0 ; :: thesis: contradiction

hence contradiction by GLIB_001:67; :: thesis: verum

end;

suppose len (W2 .vertexSeq()) = 1 ; :: thesis: contradiction

then (W2 .length()) + 1 = 0 + 1 by GLIB_009:28;
hence contradiction by A2, GLIB_001:def 26; :: thesis: verum

end;

suppose len (W2 .vertexSeq()) = 2 ; :: thesis: contradiction

then (W2 .length()) + 1 = 1 + 1 by GLIB_009:28;
then A5: len W2 = (2 * 1) + 1 by GLIB_001:112;
then ( 1 is odd & 1 < len W2 ) ;
then A6: W2 . (1 + 1) Joins W2 . 1,W2 . (1 + 2), createGraph e by GLIB_001:def 3;
W2 . 1 = W2 .first() by GLIB_001:def 6
.= W2 .last() by A2, GLIB_001:def 24
.= W2 . 3 by A5, GLIB_001:def 7 ;
then e Joins W2 . 1,W2 . 1, createGraph e by A6, Th16;
then e in (createGraph e) .loops() by GLIB_009:def 2;
hence contradiction by A1, GLIB_009:48, TARSKI:def 3; :: thesis: verum

end;

suppose len (W2 .vertexSeq()) = 3 ; :: thesis: contradiction

then (W2 .length()) + 1 = 2 + 1 by GLIB_009:28;
then len (W2 .edgeSeq()) = 2 by GLIB_001:def 18;
then A7: 2 <= (createGraph e) .size() by A2, GLIB_001:144;
the_Edges_of (createGraph e) = {e} by Th13;
then card (the_Edges_of (createGraph e)) = 1 by CARD_1:30;
then (createGraph e) .size() = 1 by GLIB_000:def 25;
hence contradiction by A7; :: thesis: verum

end;

end;