G .size() = card (the_Edges_of G) ;
hence G .size() is Element of NAT ; :: thesis: verum