let c be Cardinal; :: thesis: for G being c -regular _Graph holds 2 *` (G .size()) = c *` (G .order())
let G be c -regular _Graph; :: thesis: 2 *` (G .size()) = c *` (G .order())

per cases ( c is empty or not c is empty ) ;

suppose c is empty ; :: thesis: 2 *` (G .size()) = c *` (G .order())

then A1: ( c *` (G .order()) = 0 & G is edgeless ) by CARD_2:20;
then G .size() = 0 ;
hence 2 *` (G .size()) = c *` (G .order()) by A1, CARD_2:20; :: thesis: verum

end;

suppose A2: not c is empty ; :: thesis: 2 *` (G .size()) = c *` (G .order())

A3: for A being set st A in H₈(G) holds
card A = c

proof

let A be set ; :: thesis: ( A in H₈(G) implies card A = c )
assume A in H₈(G) ; :: thesis: card A = c
then consider v being Vertex of G such that
A4: ( A = H₆(G,v) \/ H₇(G,v) & not v is isolated ) ;
thus card A = c by A4, Lm11; :: thesis: verum

end;

thus 2 *` (G .size()) = (G .size()) *` (card {0,1}) by CARD_2:57
.= card [:(card (the_Edges_of G)),(card {0,1}):] by CARD_2:def 2
.= card [:(the_Edges_of G),{0,1}:] by CARD_2:7
.= card (dom H₅(G)) by Lm9
.= card (rng H₅(G)) by Lm8, CARD_1:70
.= card (union H₈(G)) by Lm16
.= c *` (card H<sub>8</sub>(G)) by A3, Lm14, Th56
.= c *` (G .order()) by A2, Lm15 ; :: thesis: verum

end;

end;