let G be _Graph; :: thesis: ( G is connected iff G .allSpanningTrees() <> {} )

hereby :: thesis: ( G .allSpanningTrees() <> {} implies G is connected )

assume G is connected ; :: thesis: G .allSpanningTrees() <> {}
then reconsider G0 = G as connected _Graph ;
the spanning Tree-like plain Subgraph of G0 in G .allSpanningTrees() by Th168;
hence G .allSpanningTrees() <> {} ; :: thesis: verum

end;

assume A1: G .allSpanningTrees() <> {} ; :: thesis: G is connected
set x = the Element of G .allSpanningTrees() ;
reconsider H = the Element of G .allSpanningTrees() as spanning acyclic plain Subgraph of G by A1, Th168;
H is connected by A1, Th168;
hence G is connected by GLIB_002:23; :: thesis: verum