hereby :: thesis: ( ex n being Nat st G is n -regular implies G is regular )

assume G is regular ; :: thesis: ex n being Nat st G is n -regular
then consider c being Cardinal such that
A1: G is c -regular ;
set v = the Vertex of G;
( the Vertex of G .degree() = c & the Vertex of G .degree() is finite ) by A1;
then reconsider n = c as Nat ;
take n = n; :: thesis: G is n -regular
thus G is n -regular by A1; :: thesis: verum

end;

thus ( ex n being Nat st G is n -regular implies G is regular ) ; :: thesis: verum