let a, b, c be Nat; :: thesis: ( a + b <= c implies ( a <= c & b <= c ) )
assume A1: a + b <= c ; :: thesis: ( a <= c & b <= c )
( a <= a + b & b <= a + b ) by NAT_1:11;
hence ( a <= c & b <= c ) by A1, XXREAL_0:2; :: thesis: verum