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