let GF be Graph-yielding Function; :: thesis: ( GF is loopless & GF is non-Dmulti implies GF is Dsimple )
per cases ( GF is empty or not GF is empty ) ;
suppose GF is empty ; :: thesis: ( GF is loopless & GF is non-Dmulti implies GF is Dsimple )
hence ( GF is loopless & GF is non-Dmulti implies GF is Dsimple ) ; :: thesis: verum
end;
suppose not GF is empty ; :: thesis: ( GF is loopless & GF is non-Dmulti implies GF is Dsimple )
hence ( GF is loopless & GF is non-Dmulti implies GF is Dsimple ) ; :: thesis: verum
end;
end;