G .numComponents() = card (G .componentSet()) ;
hence G .numComponents() is non empty Element of NAT ; :: thesis: verum