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