let c be Cardinal; :: thesis: for G being c -regular _Graph
for v being Vertex of G holds card (H₆(G,v) \/ H₇(G,v)) = c
let G be c -regular _Graph; :: thesis: for v being Vertex of G holds card (H₆(G,v) \/ H₇(G,v)) = c
let v be Vertex of G; :: thesis: card (H₆(G,v) \/ H₇(G,v)) = c
thus card (H₆(G,v) \/ H₇(G,v)) = (card H₆(G,v)) +` (card H<sub>7</sub>(G,v)) by Lm10, CARD_2:35
.= (card H<sub>6</sub>(G,v)) +` (card [:[:{v},(v .edgesIn()):],{1}:]) by ZFMISC_1:def 3
.= (card H₆(G,v)) +` (card [:{v},(v .edgesIn()):]) by CARD_1:69
.= (card H<sub>6</sub>(G,v)) +` (card [:(v .edgesIn()),{v}:]) by CARD_2:4
.= (card H₆(G,v)) +` (v .inDegree()) by CARD_1:69
.= (card [:[:{v},(v .edgesOut()):],{0}:]) +` (v .inDegree()) by ZFMISC_1:def 3
.= (card [:{v},(v .edgesOut()):]) +` (v .inDegree()) by CARD_1:69
.= (card [:(v .edgesOut()),{v}:]) +` (v .inDegree()) by CARD_2:4
.= v .degree() by CARD_1:69
.= c by Def4 ; :: thesis: verum