take <* the plain _Graph*> ; :: thesis: ( not <* the plain _Graph*> is empty & <* the plain _Graph*> is plain )
thus ( not <* the plain _Graph*> is empty & <* the plain _Graph*> is plain ) ; :: thesis: verum