let i, j be Nat; :: thesis: ( i <= j & j <= i + 7 & not j = i & not j = i + 1 & not j = i + 2 & not j = i + 3 & not j = i + 4 & not j = i + 5 & not j = i + 6 implies j = i + 7 )
assume A0: ( i <= j & j <= i + 7 ) ; :: thesis: ( j = i or j = i + 1 or j = i + 2 or j = i + 3 or j = i + 4 or j = i + 5 or j = i + 6 or j = i + 7 )

now :: thesis: ( ( j <= i + 3 & ( j = i or j = i + 1 or j = i + 2 or j = i + 3 ) ) or ( j > i + 3 & ( j = i + 4 or j = i + 5 or j = i + 6 or j = i + 7 ) ) )

per cases ( j <= i + 3 or j > i + 3 ) ;

case j <= i + 3 ; :: thesis: ( j = i or j = i + 1 or j = i + 2 or j = i + 3 )

hence ( j = i or j = i + 1 or j = i + 2 or j = i + 3 ) by Lmseg4, A0; :: thesis: verum

end;

case A2: j > i + 3 ; :: thesis: ( j = i + 4 or j = i + 5 or j = i + 6 or j = i + 7 )

(i + 3) + 1 <= j by A2, NAT_1:13;
then ( j = i + 4 or j = (i + 4) + 1 or j = (i + 4) + 2 or j = (i + 4) + 3 ) by Lmseg4, A0;
hence ( j = i + 4 or j = i + 5 or j = i + 6 or j = i + 7 ) ; :: thesis: verum

end;

end;

end;

hence ( j = i or j = i + 1 or j = i + 2 or j = i + 3 or j = i + 4 or j = i + 5 or j = i + 6 or j = i + 7 ) ; :: thesis: verum