let c be Cardinal; :: thesis: for G being _Graph holds
( G is c -regular iff for C being Component of G holds C is c -regular )
let G be _Graph; :: thesis: ( G is c -regular iff for C being Component of G holds C is c -regular )
thus ( G is c -regular implies for C being Component of G holds C is c -regular ) :: thesis: ( ( for C being Component of G holds C is c -regular ) implies G is c -regular )

proof

assume A1: G is c -regular ; :: thesis: for C being Component of G holds C is c -regular
let C be Component of G; :: thesis: C is c -regular
let w be Vertex of C; :: according to GLIB_016:def 4 :: thesis: w .degree() = c
the_Vertices_of C c= the_Vertices_of G ;
then reconsider v = w as Vertex of G by TARSKI:def 3;
thus w .degree() = v .degree() by GLIBPRE0:44
.= c by A1 ; :: thesis: verum

end;

assume A2: for C being Component of G holds C is c -regular ; :: thesis: G is c -regular
let v be Vertex of G; :: according to GLIB_016:def 4 :: thesis: v .degree() = c
set C = the inducedSubgraph of G,(G .reachableFrom v);
A3: the_Vertices_of the inducedSubgraph of G,(G .reachableFrom v) = G .reachableFrom v by GLIB_000:def 37;
A4: the inducedSubgraph of G,(G .reachableFrom v) is c -regular by A2;
v in G .reachableFrom v by GLIB_002:9;
then reconsider w = v as Vertex of the inducedSubgraph of G,(G .reachableFrom v) by A3;
thus v .degree() = w .degree() by GLIBPRE0:44
.= c by A4 ; :: thesis: verum