thus not G .allTrees() is empty by Th142; :: thesis: ( G .allTrees() is \/-tolerating & G .allTrees() is plain & G .allTrees() is Tree-like & G .allTrees() is simple )
thus ( G .allTrees() is \/-tolerating & G .allTrees() is plain ) ; :: thesis: ( G .allTrees() is Tree-like & G .allTrees() is simple )
for H being _Graph st H in G .allTrees() holds
H is Tree-like by Th138;
hence G .allTrees() is Tree-like by GLIB_014:def 10; :: thesis: G .allTrees() is simple
hence G .allTrees() is simple ; :: thesis: verum