let G2 be Supergraph of G; :: thesis: not G2 is non-multi
A1: G is Subgraph of G2 by Th61;
assume G2 is non-multi ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum