G .order() = card (the_Vertices_of G) ;
hence G .order() is non zero Element of NAT ; :: thesis: verum