let G2 be Subgraph of G; :: thesis: G2 is non-multi

now

let e1, e2, v1, v2 be set ; :: thesis: ( e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 implies e1 = e2 )
assume ( e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 ) ; :: thesis: e1 = e2
then ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) by Lm5;
hence e1 = e2 by Def22; :: thesis: verum

end;

hence G2 is non-multi by Def22; :: thesis: verum