thus not G .allForests() is empty by Th82; :: thesis: ( G .allForests() is \/-tolerating & G .allForests() is plain & G .allForests() is acyclic & G .allForests() is simple )
thus ( G .allForests() is \/-tolerating & G .allForests() is plain ) ; :: thesis: ( G .allForests() is acyclic & G .allForests() is simple )
for H being _Graph st H in G .allForests() holds
H is acyclic by Th78;
hence G .allForests() is acyclic by GLIB_014:def 8; :: thesis: G .allForests() is simple
hence G .allForests() is simple ; :: thesis: verum