v .degree() = card ((v .inDegree() ) +^ (v .outDegree() )) by CARD_2:def 1
.= card ((v .inDegree() ) + (v .outDegree() )) by CARD_2:49
.= (v .inDegree() ) + (v .outDegree() ) by CARD_1:def 5 ;
hence ( v .degree() is Element of NAT & ( for b₁ being Element of NAT holds
( b₁ = v .degree() iff b₁ = (v .inDegree() ) + (v .outDegree() ) ) ) ) ; :: thesis: verum