let GF be Graph-yielding Function; :: thesis: ( GF is empty implies ( GF is finite & GF is loopless & GF is trivial & GF is non-trivial & GF is non-multi & GF is non-Dmulti & GF is simple & GF is Dsimple ) )
assume GF is empty ; :: thesis: ( GF is finite & GF is loopless & GF is trivial & GF is non-trivial & GF is non-multi & GF is non-Dmulti & GF is simple & GF is Dsimple )
hence ( GF is finite & GF is loopless & GF is trivial & GF is non-trivial & GF is non-multi & GF is non-Dmulti & GF is simple & GF is Dsimple ) ; :: thesis: verum