v .degree() = card ((v .inDegree()) +^ (v .outDegree())) by CARD_2:def 1
.= card ((v .inDegree()) + (v .outDegree())) by CARD_2:36
.= (v .inDegree()) + (v .outDegree()) ;
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