Lm1:
for a, b being Cardinal st a c= b & a <> b holds
a +` 1 c= b
Lm2:
for a, b, c being Cardinal st c c= a & c c= b & a in c +` 2 & not a c= b holds
b = c
Lm3:
for G being _Graph st ex v being Vertex of G st v .degree() = G .supDegree() holds
G is with_max_degree
Lm4:
for G being _Graph st ex v being Vertex of G st v .inDegree() = G .supInDegree() holds
G is with_max_in_degree
Lm5:
for G being _Graph st ex v being Vertex of G st v .outDegree() = G .supOutDegree() holds
G is with_max_out_degree
Lm6:
for a, b, c being Cardinal st a c= c & b c= c & c c< a +` 2 & not b c= a holds
b = c
Lm7:
for a, b being Cardinal st a in b +` 1 holds
a c= b