let G be _Graph; :: thesis: G .allSpanningTrees() = (G .allSpanningSG()) /\ (G .allTrees())

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

let x be object ; :: thesis: ( ( x in G .allSpanningTrees() implies ( x in G .allSpanningSG() & x in G .allTrees() ) ) & ( x in G .allSpanningSG() & x in G .allTrees() implies x in G .allSpanningTrees() ) )

hereby :: thesis: ( x in G .allSpanningSG() & x in G .allTrees() implies x in G .allSpanningTrees() )

assume A1: x in G .allSpanningTrees() ; :: thesis: ( x in G .allSpanningSG() & x in G .allTrees() )
then reconsider H = x as spanning acyclic plain Subgraph of G by Th168;
H is connected by A1, Th168;
hence ( x in G .allSpanningSG() & x in G .allTrees() ) by Th60, Th138; :: thesis: verum

end;

assume A2: ( x in G .allSpanningSG() & x in G .allTrees() ) ; :: thesis: x in G .allSpanningTrees()
then reconsider H = x as spanning acyclic plain Subgraph of G by Th60;
H is connected by A2;
hence x in G .allSpanningTrees() by Th168; :: thesis: verum

end;

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