let GF be Graph-yielding Function; :: thesis: ( GF is Dsimple implies ( GF is loopless & GF is non-Dmulti ) )

per cases ( GF is empty or not GF is empty ) ;

suppose GF is empty ; :: thesis: ( GF is Dsimple implies ( GF is loopless & GF is non-Dmulti ) )

hence ( GF is Dsimple implies ( GF is loopless & GF is non-Dmulti ) ) ; :: thesis: verum

end;

suppose not GF is empty ; :: thesis: ( GF is Dsimple implies ( GF is loopless & GF is non-Dmulti ) )

hence ( GF is Dsimple implies ( GF is loopless & GF is non-Dmulti ) ) ; :: thesis: verum

end;

end;