let n be natural number ; :: thesis: ( n is m _or_greater implies not n is trivial )
assume A1: n is m _or_greater ; :: thesis: not n is trivial
m >= 2 by NAT_2:29;
hence not n is trivial by A1, XXREAL_0:2; :: thesis: verum