let G1, G2 be _Graph; for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is directed & F is weak_SG-embedding holds
( v .inDegree() c= ((F _V) /. v) .inDegree() & v .outDegree() c= ((F _V) /. v) .outDegree() )
let F be PGraphMapping of G1,G2; for v being Vertex of G1 st F is directed & F is weak_SG-embedding holds
( v .inDegree() c= ((F _V) /. v) .inDegree() & v .outDegree() c= ((F _V) /. v) .outDegree() )
let v be Vertex of G1; ( F is directed & F is weak_SG-embedding implies ( v .inDegree() c= ((F _V) /. v) .inDegree() & v .outDegree() c= ((F _V) /. v) .outDegree() ) )
assume A1:
( F is directed & F is weak_SG-embedding )
; ( v .inDegree() c= ((F _V) /. v) .inDegree() & v .outDegree() c= ((F _V) /. v) .outDegree() )
then A2:
dom (F _E) = the_Edges_of G1
by GLIB_010:def 11;
set f = (F _E) | (v .edgesIn());
A3: dom ((F _E) | (v .edgesIn())) =
(dom (F _E)) /\ (v .edgesIn())
by RELAT_1:61
.=
v .edgesIn()
by A2, XBOOLE_1:28
;
A4:
rng ((F _E) | (v .edgesIn())) = (F _E) .: (v .edgesIn())
by RELAT_1:115;
dom (F _V) = the_Vertices_of G1
by A1, GLIB_010:def 11;
then
(F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn()
by A1, Th87;
then A5:
card ((F _E) .: (v .edgesIn())) c= card (((F _V) /. v) .edgesIn())
by CARD_1:11;
(F _E) | (v .edgesIn()) is one-to-one
by A1, FUNCT_1:52;
hence
v .inDegree() c= ((F _V) /. v) .inDegree()
by A3, A4, A5, CARD_1:70; v .outDegree() c= ((F _V) /. v) .outDegree()
set f = (F _E) | (v .edgesOut());
A6: dom ((F _E) | (v .edgesOut())) =
(dom (F _E)) /\ (v .edgesOut())
by RELAT_1:61
.=
v .edgesOut()
by A2, XBOOLE_1:28
;
A7:
rng ((F _E) | (v .edgesOut())) = (F _E) .: (v .edgesOut())
by RELAT_1:115;
dom (F _V) = the_Vertices_of G1
by A1, GLIB_010:def 11;
then
(F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut()
by A1, Th87;
then A8:
card ((F _E) .: (v .edgesOut())) c= card (((F _V) /. v) .edgesOut())
by CARD_1:11;
(F _E) | (v .edgesOut()) is one-to-one
by A1, FUNCT_1:52;
hence
v .outDegree() c= ((F _V) /. v) .outDegree()
by A6, A7, A8, CARD_1:70; verum