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;