let G be _finite _Graph; :: thesis: G .order() >= 1
0 + 1 < (G .order()) + 1 by NAT_1:3, XREAL_1:8;
hence G .order() >= 1 by NAT_1:13; :: thesis: verum