:: deftheorem defines .order() GLIB_000:def 24 :
for G being _Graph holds G .order() = card (the_Vertices_of G);