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