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:9;
hence i >= k by XREAL_1:8; :: thesis: verum