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 ) )
assume G2 is _trivial ; :: thesis: G1 is _trivial
then card (the_Vertices_of G2) = 1 by GLIB_000:def 19;
then A2: G2 .order() = 1 by GLIB_000:def 24;
G1 .order() = 1
proof
assume G1 .order() <> 1 ; :: thesis: contradiction
then G1 .order() in 1 by A1, A2, Th45, CARD_1:3;
then G1 .order() = 0 by CARD_1:49, TARSKI:def 1;
then card (the_Vertices_of G1) = 0 by GLIB_000:def 24;
hence contradiction ; :: thesis: verum
end;
then card (the_Vertices_of G1) = 1 by GLIB_000:def 24;
hence G1 is _trivial by GLIB_000:def 19; :: thesis: verum
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 A1, Def11;
( v1 in the_Vertices_of G1 & v2 in the_Vertices_of G1 ) by A5, GLIB_000:13;
then ( v1 in dom (F _V) & v2 in dom (F _V) ) by A1, Def11;
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 A1, A4, A6, GLIB_000:def 20, FUNCT_1:def 4; :: 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 )
assume G2 is simple ; :: thesis: G1 is simple
then ( G1 is loopless & G1 is non-multi ) by A3, A1, Th35;
hence G1 is simple ; :: thesis: verum
end;
assume G2 is _finite ; :: thesis: G1 is _finite
then ( card (the_Vertices_of G2) is finite & card (the_Edges_of G2) is finite ) ;
then A7: ( G2 .order() is finite & G2 .size() is finite ) by GLIB_000:def 24, GLIB_000:def 25;
( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() ) by A1, Th45;
then ( card (the_Vertices_of G1) is finite & card (the_Edges_of G1) is finite ) by A7, GLIB_000:def 24, GLIB_000:def 25;
then ( the_Vertices_of G1 is finite & the_Edges_of G1 is finite ) ;
hence G1 is _finite by GLIB_000:def 17; :: thesis: verum