:: deftheorem Def3 defines -vertex GLIB_013:def 3 :
for c being Cardinal
for G being _Graph holds
( G is c -vertex iff G .order() = c );