let G1 be Supergraph of G; :: thesis: not G1 is Dsimple
per cases ( not G is non-Dmulti or not G is loopless ) ;
suppose not G is non-Dmulti ; :: thesis: not G1 is Dsimple
hence not G1 is Dsimple ; :: thesis: verum
end;
suppose not G is loopless ; :: thesis: not G1 is Dsimple
hence not G1 is Dsimple ; :: thesis: verum
end;
end;