let G1, G2 be _Graph; 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; ( 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
; ( ( 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 ) )
thus A3:
( G2 is non-multi implies G1 is non-multi )
( ( G2 is simple implies G1 is simple ) & ( G2 is _finite implies G1 is _finite ) )proof
assume A4:
G2 is
non-multi
;
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 ;
( 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 )
;
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;
verum
end;
hence
G1 is
non-multi
by GLIB_000:def 20;
verum
end;
assume
G2 is _finite
; 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; verum