let j, k, l be Nat; :: thesis: ( ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) implies ( 1 <= j & j <= l + k ) )
assume A1: ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) ; :: thesis: ( 1 <= j & j <= l + k )

per cases ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) by A1;

suppose A2: ( 1 <= j & j <= l ) ; :: thesis: ( 1 <= j & j <= l + k )

l + 0 <= l + k by XREAL_1:7;
hence ( 1 <= j & j <= l + k ) by A2, XXREAL_0:2; :: thesis: verum

end;

suppose A3: ( l + 1 <= j & j <= l + k ) ; :: thesis: ( 1 <= j & j <= l + k )

0 + 1 <= l + 1 by XREAL_1:7;
hence ( 1 <= j & j <= l + k ) by A3, XXREAL_0:2; :: thesis: verum

end;

end;