let G1 be Subgraph of G; :: thesis: G1 is non-Dmulti
let e1, e2, v1, v2 be object ; :: according to GLIB_000:def 21 :: thesis: ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 implies e1 = e2 )
reconsider w1 = v1, w2 = v2 as set by TARSKI:1;
assume ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 ) ; :: thesis: e1 = e2
then ( e1 DJoins w1,w2,G1 & e2 DJoins w1,w2,G1 ) ;
then ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) by Th72;
hence e1 = e2 by Def21; :: thesis: verum