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;