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