take the non empty Graph-yielding non acyclic Function ; :: thesis: ( not the non empty Graph-yielding non acyclic Function is empty & not the non empty Graph-yielding non acyclic Function is edgeless )
thus ( not the non empty Graph-yielding non acyclic Function is empty & not the non empty Graph-yielding non acyclic Function is edgeless ) ; :: thesis: verum