let G1, G2 be loopless connected _Graph; :: thesis: ( G1 == G2 iff G1 .allSpanningTrees() = G2 .allSpanningTrees() )

hereby :: thesis: ( G1 .allSpanningTrees() = G2 .allSpanningTrees() implies G1 == G2 )

assume G1 == G2 ; :: thesis: G1 .allSpanningTrees() = G2 .allSpanningTrees()
then G2 is removeLoops of G1 by GLIB_009:58;
hence G1 .allSpanningTrees() = G2 .allSpanningTrees() by Th176; :: thesis: verum

end;

assume G1 .allSpanningTrees() = G2 .allSpanningTrees() ; :: thesis: G1 == G2
then ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) by Th175;
hence G1 == G2 by GLIB_000:87; :: thesis: verum