let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is directed & F is weak_SG-embedding holds

( ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G2 is Dsimple implies G1 is Dsimple ) )

let F be PGraphMapping of G1,G2; :: thesis: ( F is directed & F is weak_SG-embedding implies ( ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G2 is Dsimple implies G1 is Dsimple ) ) )

assume A1: ( F is directed & F is weak_SG-embedding ) ; :: thesis: ( ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G2 is Dsimple implies G1 is Dsimple ) )

thus A2: ( G2 is non-Dmulti implies G1 is non-Dmulti ) :: thesis: ( G2 is Dsimple implies G1 is Dsimple )

then ( G1 is loopless & G1 is non-Dmulti ) by A2, A1, Th35;

hence G1 is Dsimple ; :: thesis: verum

( ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G2 is Dsimple implies G1 is Dsimple ) )

let F be PGraphMapping of G1,G2; :: thesis: ( F is directed & F is weak_SG-embedding implies ( ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G2 is Dsimple implies G1 is Dsimple ) ) )

assume A1: ( F is directed & F is weak_SG-embedding ) ; :: thesis: ( ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G2 is Dsimple implies G1 is Dsimple ) )

thus A2: ( G2 is non-Dmulti implies G1 is non-Dmulti ) :: thesis: ( G2 is Dsimple implies G1 is Dsimple )

proof

assume
G2 is Dsimple
; :: thesis: G1 is Dsimple
assume A3:
G2 is non-Dmulti
; :: thesis: G1 is non-Dmulti

for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 holds

e1 = e2

end;for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 holds

e1 = e2

proof

hence
G1 is non-Dmulti
by GLIB_000:def 21; :: thesis: verum
let e1, e2, v1, v2 be object ; :: thesis: ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 implies e1 = e2 )

assume A4: ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 ) ; :: thesis: e1 = e2

then ( e1 in the_Edges_of G1 & e2 in the_Edges_of G1 ) by GLIB_000:def 14;

then A5: ( e1 in dom (F _E) & e2 in dom (F _E) ) by A1, Def11;

( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 ) by A4, GLIB_000:16;

then ( v1 in the_Vertices_of G1 & v2 in the_Vertices_of G1 ) by GLIB_000:13;

then A6: ( v1 in dom (F _V) & v2 in dom (F _V) ) by A1, Def11;

then A7: (F _E) . e1 DJoins (F _V) . v1,(F _V) . v2,G2 by A1, A4, A5;

(F _E) . e2 DJoins (F _V) . v1,(F _V) . v2,G2 by A1, A4, A5, A6;

hence e1 = e2 by A1, A3, A5, A7, FUNCT_1:def 4, GLIB_000:def 21; :: thesis: verum

end;assume A4: ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 ) ; :: thesis: e1 = e2

then ( e1 in the_Edges_of G1 & e2 in the_Edges_of G1 ) by GLIB_000:def 14;

then A5: ( e1 in dom (F _E) & e2 in dom (F _E) ) by A1, Def11;

( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 ) by A4, GLIB_000:16;

then ( v1 in the_Vertices_of G1 & v2 in the_Vertices_of G1 ) by GLIB_000:13;

then A6: ( v1 in dom (F _V) & v2 in dom (F _V) ) by A1, Def11;

then A7: (F _E) . e1 DJoins (F _V) . v1,(F _V) . v2,G2 by A1, A4, A5;

(F _E) . e2 DJoins (F _V) . v1,(F _V) . v2,G2 by A1, A4, A5, A6;

hence e1 = e2 by A1, A3, A5, A7, FUNCT_1:def 4, GLIB_000:def 21; :: thesis: verum

then ( G1 is loopless & G1 is non-Dmulti ) by A2, A1, Th35;

hence G1 is Dsimple ; :: thesis: verum