let G be _Graph; :: thesis: G .allSpanningTrees() = (G .allConnectedSG()) /\ (G .allSpanningForests())

now :: thesis: for x being object holds
( ( x in G .allSpanningTrees() implies ( x in G .allConnectedSG() & x in G .allSpanningForests() ) ) & ( x in G .allConnectedSG() & x in G .allSpanningForests() implies x in G .allSpanningTrees() ) )

let x be object ; :: thesis: ( ( x in G .allSpanningTrees() implies ( x in G .allConnectedSG() & x in G .allSpanningForests() ) ) & ( x in G .allConnectedSG() & x in G .allSpanningForests() implies x in G .allSpanningTrees() ) )

hereby :: thesis: ( x in G .allConnectedSG() & x in G .allSpanningForests() implies x in G .allSpanningTrees() )

assume x in G .allSpanningTrees() ; :: thesis: ( x in G .allConnectedSG() & x in G .allSpanningForests() )
then ( x is spanning acyclic plain Subgraph of G & x is connected _Graph ) by Th168;
hence ( x in G .allConnectedSG() & x in G .allSpanningForests() ) by Th102, Th124; :: thesis: verum

end;

assume ( x in G .allConnectedSG() & x in G .allSpanningForests() ) ; :: thesis: x in G .allSpanningTrees()
then ( x is spanning plain Subgraph of G & x is Tree-like plain Subgraph of G ) by Th102;
hence x in G .allSpanningTrees() by Th168; :: thesis: verum

end;

hence G .allSpanningTrees() = (G .allConnectedSG()) /\ (G .allSpanningForests()) by XBOOLE_0:def 4; :: thesis: verum