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