take the non empty _trivial edgeless GraphSeq ; :: thesis: ( not the non empty _trivial edgeless GraphSeq is empty & the non empty _trivial edgeless GraphSeq is Path-like )
thus ( not the non empty _trivial edgeless GraphSeq is empty & the non empty _trivial edgeless GraphSeq is Path-like ) ; :: thesis: verum