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