theorem :: GLIB_016:33
for G being _Graph holds
( G is cubic iff for v being Vertex of G holds v .degree() = 3 ) by Def4;