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

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

end;

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