let k, n be Nat; :: thesis: ( k > 0 implies not n in GreaterOrEqualsNumbers (n + k) )
assume k > 0 ; :: thesis: not n in GreaterOrEqualsNumbers (n + k)
then n + 0 < n + k by XREAL_1:8;
hence not n in GreaterOrEqualsNumbers (n + k) by Th56; :: thesis: verum