let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
( ( G2 is _trivial implies G1 is _trivial ) & ( G2 is non-multi implies G1 is non-multi ) & ( G2 is simple implies G1 is simple ) & ( G2 is _finite implies G1 is _finite ) )

let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding implies ( ( G2 is _trivial implies G1 is _trivial ) & ( G2 is non-multi implies G1 is non-multi ) & ( G2 is simple implies G1 is simple ) & ( G2 is _finite implies G1 is _finite ) ) )
assume A1: F is weak_SG-embedding ; :: thesis: ( ( G2 is _trivial implies G1 is _trivial ) & ( G2 is non-multi implies G1 is non-multi ) & ( G2 is simple implies G1 is simple ) & ( G2 is _finite implies G1 is _finite ) )
hereby :: thesis: ( ( G2 is non-multi implies G1 is non-multi ) & ( G2 is simple implies G1 is simple ) & ( G2 is _finite implies G1 is _finite ) ) end;
thus A3: ( G2 is non-multi implies G1 is non-multi ) :: thesis: ( ( G2 is simple implies G1 is simple ) & ( G2 is _finite implies G1 is _finite ) )
proof
assume A4: G2 is non-multi ; :: thesis: G1 is non-multi
for e1, e2, v1, v2 being object st e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 holds
e1 = e2
proof
let e1, e2, v1, v2 be object ; :: thesis: ( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 implies e1 = e2 )
assume A5: ( e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 ) ; :: thesis: e1 = e2
then ( e1 in the_Edges_of G1 & e2 in the_Edges_of G1 ) by GLIB_000:def 13;
then A6: ( e1 in dom (F _E) & e2 in dom (F _E) ) by ;
( v1 in the_Vertices_of G1 & v2 in the_Vertices_of G1 ) by ;
then ( v1 in dom (F _V) & v2 in dom (F _V) ) by ;
then ( (F _E) . e1 Joins (F _V) . v1,(F _V) . v2,G2 & (F _E) . e2 Joins (F _V) . v1,(F _V) . v2,G2 ) by A5, A6, Th4;
hence e1 = e2 by ; :: thesis: verum
end;
hence G1 is non-multi by GLIB_000:def 20; :: thesis: verum
end;
hereby :: thesis: ( G2 is _finite implies G1 is _finite ) end;
assume G2 is _finite ; :: thesis: G1 is _finite
then ( card () is finite & card () is finite ) ;
then A7: ( G2 .order() is finite & G2 .size() is finite ) by ;
( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() ) by ;
then ( card () is finite & card () is finite ) by ;
then ( the_Vertices_of G1 is finite & the_Edges_of G1 is finite ) ;
hence G1 is _finite by GLIB_000:def 17; :: thesis: verum