let G be _Graph; :: thesis: ( the_Edges_of G = G .loops() iff for H being removeLoops of G holds G .allSpanningForests() = {(H | _GraphSelectors)} )

hereby :: thesis: ( ( for H being removeLoops of G holds G .allSpanningForests() = {(H | _GraphSelectors)} ) implies the_Edges_of G = G .loops() )

assume A1: the_Edges_of G = G .loops() ; :: thesis: for H being removeLoops of G holds G .allSpanningForests() = {(H | _GraphSelectors)}
let H be removeLoops of G; :: thesis: G .allSpanningForests() = {(H | _GraphSelectors)}
A2: H is edgeless by A1;

now :: thesis: for x being object holds
( ( x in G .allSpanningForests() implies x = H | _GraphSelectors ) & ( x = H | _GraphSelectors implies x in G .allSpanningForests() ) )

let x be object ; :: thesis: ( ( x in G .allSpanningForests() implies x = H | _GraphSelectors ) & ( x = H | _GraphSelectors implies x in G .allSpanningForests() ) )

hereby :: thesis: ( x = H | _GraphSelectors implies x in G .allSpanningForests() )

assume x in G .allSpanningForests() ; :: thesis: x = H | _GraphSelectors
then reconsider H9 = x as spanning acyclic plain Subgraph of G by Th102;

now :: thesis: ( the_Vertices_of H9 = the_Vertices_of H & the_Edges_of H9 = the_Edges_of H & the_Source_of H9 = the_Source_of H & the_Target_of H9 = the_Target_of H )

thus the_Vertices_of H9 = the_Vertices_of G by GLIB_000:def 33
.= the_Vertices_of H by GLIB_000:def 33 ; :: thesis: ( the_Edges_of H9 = the_Edges_of H & the_Source_of H9 = the_Source_of H & the_Target_of H9 = the_Target_of H )
A3: the_Edges_of H9 = {}

proof

assume the_Edges_of H9 <> {} ; :: thesis: contradiction
then consider e being object such that
A4: e in the_Edges_of H9 by XBOOLE_0:def 1;
set v = (the_Source_of H9) . e;
set w = (the_Target_of H9) . e;
A5: e Joins (the_Source_of H9) . e,(the_Target_of H9) . e,H9 by A4, GLIB_000:def 13;

per cases ( (the_Source_of H9) . e = (the_Target_of H9) . e or (the_Source_of H9) . e <> (the_Target_of H9) . e ) ;

suppose (the_Source_of H9) . e = (the_Target_of H9) . e ; :: thesis: contradiction

then H9 .walkOf (((the_Source_of H9) . e),e,((the_Target_of H9) . e)) is Cycle-like by A5, GLIB_001:156;
hence contradiction by GLIB_002:def 2; :: thesis: verum

end;

suppose A6: (the_Source_of H9) . e <> (the_Target_of H9) . e ; :: thesis: contradiction

e Joins (the_Source_of H9) . e,(the_Target_of H9) . e,G by A5, GLIB_000:72;
hence contradiction by A1, A4, A6, GLIB_009:46; :: thesis: verum

end;

end;

end;

hence the_Edges_of H9 = the_Edges_of H by A2; :: thesis: ( the_Source_of H9 = the_Source_of H & the_Target_of H9 = the_Target_of H )
hence ( the_Source_of H9 = the_Source_of H & the_Target_of H9 = the_Target_of H ) by A3; :: thesis: verum

end;

then A7: H9 == H by GLIB_000:def 34;
H == H | _GraphSelectors by GLIB_000:128;
hence x = H | _GraphSelectors by A7, GLIB_000:85, GLIB_009:44; :: thesis: verum

end;

assume x = H | _GraphSelectors ; :: thesis: x in G .allSpanningForests()
hence x in G .allSpanningForests() by A2, Th104; :: thesis: verum

end;

hence G .allSpanningForests() = {(H | _GraphSelectors)} by TARSKI:def 1; :: thesis: verum

end;

assume A8: for H being removeLoops of G holds G .allSpanningForests() = {(H | _GraphSelectors)} ; :: thesis: the_Edges_of G = G .loops()

now :: thesis: for e being object st e in the_Edges_of G holds
e in G .loops()

let e be object ; :: thesis: ( e in the_Edges_of G implies e in G .loops() )
assume A9: ( e in the_Edges_of G & not e in G .loops() ) ; :: thesis: contradiction
set H = the removeLoops of G;
set H9 = the removeEdges of G,(the_Edges_of G);
A10: ( the removeLoops of G == the removeLoops of G | _GraphSelectors & the removeEdges of G,(the_Edges_of G) == the removeEdges of G,(the_Edges_of G) | _GraphSelectors ) by GLIB_000:128;
the_Edges_of the removeLoops of G = (the_Edges_of G) \ (G .loops()) by GLIB_000:53;
then e in the_Edges_of the removeLoops of G by A9, XBOOLE_0:def 5;
then A11: e in the_Edges_of ( the removeLoops of G | _GraphSelectors) by A10, GLIB_000:def 34;
not e in the_Edges_of the removeEdges of G,(the_Edges_of G) ;
then not e in the_Edges_of ( the removeEdges of G,(the_Edges_of G) | _GraphSelectors) by A10, GLIB_000:def 34;
then A12: the removeLoops of G | _GraphSelectors <> the removeEdges of G,(the_Edges_of G) | _GraphSelectors by A11;
A13: the removeLoops of G | _GraphSelectors in {( the removeLoops of G | _GraphSelectors)} by TARSKI:def 1;
the removeEdges of G,(the_Edges_of G) | _GraphSelectors in G .allSpanningForests() by Th104;
then the removeEdges of G,(the_Edges_of G) | _GraphSelectors in {( the removeLoops of G | _GraphSelectors)} by A8;
then {( the removeLoops of G | _GraphSelectors),( the removeEdges of G,(the_Edges_of G) | _GraphSelectors)} c= {( the removeLoops of G | _GraphSelectors)} by A13, ZFMISC_1:32;
hence contradiction by A12, ZFMISC_1:20; :: thesis: verum

end;

then the_Edges_of G c= G .loops() by TARSKI:def 3;
hence the_Edges_of G = G .loops() by XBOOLE_0:def 10; :: thesis: verum