let G1 be _finite _Graph; :: thesis: for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() )
let G2 be Subgraph of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() ) )
assume A1: v1 = v2 ; :: thesis: ( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() )
then v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) by Th79;
hence A2: v2 .inDegree() <= v1 .inDegree() by NAT_1:43, XBOOLE_1:17; :: thesis: ( v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() )
A3: v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) by A1, Th79;
hence v2 .outDegree() <= v1 .outDegree() by NAT_1:43, XBOOLE_1:17; :: thesis: v2 .degree() <= v1 .degree()
v2 .outDegree() <= card (v1 .edgesOut()) by A3, NAT_1:43, XBOOLE_1:17;
hence v2 .degree() <= v1 .degree() by A2, XREAL_1:7; :: thesis: verum