take <* the finite non trivial Tree-like _Graph*> ; :: thesis: ( not <* the finite non trivial Tree-like _Graph*> is empty & <* the finite non trivial Tree-like _Graph*> is finite & <* the finite non trivial Tree-like _Graph*> is loopless & <* the finite non trivial Tree-like _Graph*> is non-trivial & <* the finite non trivial Tree-like _Graph*> is non-multi & <* the finite non trivial Tree-like _Graph*> is non-Dmulti & <* the finite non trivial Tree-like _Graph*> is simple & <* the finite non trivial Tree-like _Graph*> is Dsimple & <* the finite non trivial Tree-like _Graph*> is connected & <* the finite non trivial Tree-like _Graph*> is acyclic & <* the finite non trivial Tree-like _Graph*> is Tree-like )
thus ( not <* the finite non trivial Tree-like _Graph*> is empty & <* the finite non trivial Tree-like _Graph*> is finite & <* the finite non trivial Tree-like _Graph*> is loopless & <* the finite non trivial Tree-like _Graph*> is non-trivial & <* the finite non trivial Tree-like _Graph*> is non-multi & <* the finite non trivial Tree-like _Graph*> is non-Dmulti & <* the finite non trivial Tree-like _Graph*> is simple & <* the finite non trivial Tree-like _Graph*> is Dsimple & <* the finite non trivial Tree-like _Graph*> is connected & <* the finite non trivial Tree-like _Graph*> is acyclic & <* the finite non trivial Tree-like _Graph*> is Tree-like ) ; :: thesis: verum