b >= 1 by NAT_1:14;
then a + b > 0 + 1 by XREAL_1:8;
hence not a + b is trivial ; :: thesis: verum