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;