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 ) )

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

( ( 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 ) )

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 ) )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

hence G1 is _trivial by GLIB_000:def 19; :: thesis: verum

end;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

then
card (the_Vertices_of G1) = 1
by GLIB_000:def 24;
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 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

hence G1 is _trivial by GLIB_000:def 19; :: thesis: verum

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

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

e1 = e2

proof

hence
G1 is non-multi
by GLIB_000:def 20; :: thesis: verum
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;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

hereby :: thesis: ( G2 is _finite implies G1 is _finite )

assume
G2 is _finite
; :: thesis: 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;then ( G1 is loopless & G1 is non-multi ) by A3, A1, Th35;

hence G1 is simple ; :: thesis: verum

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