let G be _Graph; :: thesis: ( G is Dregular iff ( G .minInDegree() = G .supInDegree() & G .minOutDegree() = G .supOutDegree() & G .minInDegree() = G .minOutDegree() ) )

hereby :: thesis: ( G .minInDegree() = G .supInDegree() & G .minOutDegree() = G .supOutDegree() & G .minInDegree() = G .minOutDegree() implies G is Dregular )

assume G is Dregular ; :: thesis: ( G .minInDegree() = G .supInDegree() & G .minOutDegree() = G .supOutDegree() & G .minInDegree() = G .minOutDegree() )
then consider c being Cardinal such that
A1: G is c -Dregular ;
thus G .minInDegree() = c by A1, Th44
.= G .supInDegree() by A1, Th44 ; :: thesis: ( G .minOutDegree() = G .supOutDegree() & G .minInDegree() = G .minOutDegree() )
thus G .minOutDegree() = c by A1, Th44
.= G .supOutDegree() by A1, Th44 ; :: thesis: G .minInDegree() = G .minOutDegree()
thus G .minInDegree() = c by A1, Th44
.= G .minOutDegree() by A1, Th44 ; :: thesis: verum

end;

assume ( G .minInDegree() = G .supInDegree() & G .minOutDegree() = G .supOutDegree() & G .minInDegree() = G .minOutDegree() ) ; :: thesis: G is Dregular
then G is G .minInDegree() -Dregular by Th45;
hence G is Dregular ; :: thesis: verum