let i, k, l be Nat; :: thesis: ( i >= k + l implies i >= k )
assume i >= k + l ; :: thesis: i >= k
then i + l >= (k + l) + 0 by XREAL_1:7;
hence i >= k by XREAL_1:6; :: thesis: verum