:: deftheorem defines .size() GLIB_000:def 25 :
for G being _Graph holds G .size() = card (the_Edges_of G);