let G be _Graph; :: thesis: ( G is regular iff G .minDegree() = G .supDegree() )

hereby :: thesis: ( G .minDegree() = G .supDegree() implies G is regular )

assume G is regular ; :: thesis: G .minDegree() = G .supDegree()
then consider c being Cardinal such that
A1: G is c -regular ;
thus G .minDegree() = c by A1, Th22
.= G .supDegree() by A1, Th22 ; :: thesis: verum

end;

assume G .minDegree() = G .supDegree() ; :: thesis: G is regular
then G is G .minDegree() -regular by Th23;
hence G is regular ; :: thesis: verum