let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is onto & F is semi-Dcontinuous & v in dom (F _V) holds
( ((F _V) /. v) .inDegree() c= v .inDegree() & ((F _V) /. v) .outDegree() c= v .outDegree() )
let F be PGraphMapping of G1,G2; :: thesis: for v being Vertex of G1 st F is onto & F is semi-Dcontinuous & v in dom (F _V) holds
( ((F _V) /. v) .inDegree() c= v .inDegree() & ((F _V) /. v) .outDegree() c= v .outDegree() )
let v be Vertex of G1; :: thesis: ( F is onto & F is semi-Dcontinuous & v in dom (F _V) implies ( ((F _V) /. v) .inDegree() c= v .inDegree() & ((F _V) /. v) .outDegree() c= v .outDegree() ) )
assume ( F is onto & F is semi-Dcontinuous & v in dom (F _V) ) ; :: thesis: ( ((F _V) /. v) .inDegree() c= v .inDegree() & ((F _V) /. v) .outDegree() c= v .outDegree() )
then ( (F _E) .: (v .edgesIn()) = ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) = ((F _V) /. v) .edgesOut() ) by Th89;
hence ( ((F _V) /. v) .inDegree() c= v .inDegree() & ((F _V) /. v) .outDegree() c= v .outDegree() ) by CARD_1:67; :: thesis: verum