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