let c be non empty Cardinal; :: thesis: for G being c -regular _Graph holds card H₈(G) = G .order()
let G be c -regular _Graph; :: thesis: card H₈(G) = G .order()
set V = the_Vertices_of G;
deffunc H₉( object ) -> set = H₆(G, In ($1,(the_Vertices_of G))) \/ H₇(G, In ($1,(the_Vertices_of G)));
consider g being Function such that
A1: ( dom g = the_Vertices_of G & ( for x being object st x in the_Vertices_of G holds
g . x = H₉(x) ) ) from FUNCT_1:sch 3();

now :: thesis: for y being object holds
( ( y in rng g implies y in H₈(G) ) & ( y in H₈(G) implies y in rng g ) )

let y be object ; :: thesis: ( ( y in rng g implies y in H₈(G) ) & ( y in H₈(G) implies y in rng g ) )

hereby :: thesis: ( y in H₈(G) implies y in rng g )

assume y in rng g ; :: thesis: y in H₈(G)
then consider v being object such that
A2: ( v in dom g & g . v = y ) by FUNCT_1:def 3;
reconsider v = v as Vertex of G by A1, A2;
A3: g . v = H₆(G, In (v,(the_Vertices_of G))) \/ H₇(G, In (v,(the_Vertices_of G))) by A1
.= H₆(G,v) \/ H₇(G,v) ;
v .degree() = c by Def4;
then not v is isolated by GLIB_000:157;
hence y in H₈(G) by A2, A3; :: thesis: verum

end;

assume y in H₈(G) ; :: thesis: y in rng g
then consider v being Vertex of G such that
A4: ( y = H₆(G,v) \/ H₇(G,v) & not v is isolated ) ;
A5: v in dom g by A1;
g . v = H₆(G, In (v,(the_Vertices_of G))) \/ H₇(G,v) by A1
.= y by A4 ;
hence y in rng g by A5, FUNCT_1:3; :: thesis: verum

end;

then A6: rng g = H₈(G) by TARSKI:2;

now :: thesis: for x1, x2 being object st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
not x1 <> x2

let x1, x2 be object ; :: thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies not x1 <> x2 )
assume A7: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 ) ; :: thesis: not x1 <> x2
assume A8: x1 <> x2 ; :: thesis: contradiction
reconsider x1 = x1, x2 = x2 as Vertex of G by A1, A7;
A9: g . x1 = H₆(G, In (x1,(the_Vertices_of G))) \/ H₇(G, In (x1,(the_Vertices_of G))) by A1
.= H₆(G,x1) \/ H₇(G,x1) ;
A10: g . x2 = H₆(G, In (x2,(the_Vertices_of G))) \/ H₇(G, In (x2,(the_Vertices_of G))) by A1
.= H₆(G,x2) \/ H₇(G,x2) ;
( H₆(G,x1) misses H₆(G,x2) & H₇(G,x1) misses H₇(G,x2) ) by A8, Lm12, Lm13;
then A11: ( H₆(G,x1) = H₇(G,x2) & H₇(G,x1) = H₆(G,x2) ) by A7, A9, A10, XBOOLE_1:72;
( H₆(G,x1) misses H₇(G,x2) & H₇(G,x1) misses H₆(G,x2) ) by Lm10;
then A12: ( H₆(G,x1) = {} & H₇(G,x1) = {} ) by A11, XBOOLE_1:66;
x1 .degree() <> 0 by Def4;

per cases then ( x1 .edgesIn() <> {} or x1 .edgesOut() <> {} ) by GLIB_000:155, GLIB_000:157;

suppose x1 .edgesIn() <> {} ; :: thesis: contradiction

then consider e being object such that
A13: e in x1 .edgesIn() by XBOOLE_0:def 1;
( x1 in {x1} & 1 in {1} ) by TARSKI:def 1;
then [x1,e,1] in H₇(G,x1) by A13, MCART_1:69;
hence contradiction by A12; :: thesis: verum

end;

suppose x1 .edgesOut() <> {} ; :: thesis: contradiction

then consider e being object such that
A14: e in x1 .edgesOut() by XBOOLE_0:def 1;
( x1 in {x1} & 0 in {0} ) by TARSKI:def 1;
then [x1,e,0] in H₆(G,x1) by A14, MCART_1:69;
hence contradiction by A12; :: thesis: verum

end;

end;

end;

hence card H₈(G) = G .order() by A1, A6, FUNCT_1:def 4, CARD_1:70; :: thesis: verum