let G be _Graph; :: thesis: G .allTrees() = (G .allForests()) /\ (G .allConnectedSG())

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

let x be object ; :: thesis: ( ( x in G .allTrees() implies ( x in G .allForests() & x in G .allConnectedSG() ) ) & ( x in G .allForests() & x in G .allConnectedSG() implies x in G .allTrees() ) )

hereby :: thesis: ( x in G .allForests() & x in G .allConnectedSG() implies x in G .allTrees() )

assume x in G .allTrees() ; :: thesis: ( x in G .allForests() & x in G .allConnectedSG() )
then x is Tree-like plain Subgraph of G by Th138;
hence ( x in G .allForests() & x in G .allConnectedSG() ) by Th78, Th124; :: thesis: verum

end;

assume ( x in G .allForests() & x in G .allConnectedSG() ) ; :: thesis: x in G .allTrees()
hence x in G .allTrees() by Th138; :: thesis: verum

end;

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