take { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} ; :: thesis: ( not { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is empty & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is Tree-like & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is acyclic & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is connected & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is simple & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is Dsimple & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is loopless & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is non-multi & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is non-Dmulti )
thus ( not { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is empty & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is Tree-like & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is acyclic & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is connected & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is simple & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is Dsimple & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is loopless & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is non-multi & { the loopless non-multi non-Dmulti simple Dsimple connected acyclic Tree-like _Graph} is non-Dmulti ) ; :: thesis: verum