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