let i, j be Nat; :: thesis: ( i <= j & j <= i + 15 & 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 & not j = i + 7 & not j = i + 8 & not j = i + 9 & not j = i + 10 & not j = i + 11 & not j = i + 12 & not j = i + 13 & not j = i + 14 implies j = i + 15 )
assume A0: ( i <= j & j <= i + 15 ) ; :: 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 or j = i + 8 or j = i + 9 or j = i + 10 or j = i + 11 or j = i + 12 or j = i + 13 or j = i + 14 or j = i + 15 )

now :: thesis: ( ( j <= i + 7 & ( 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 ) ) or ( j > i + 7 & ( j = i + 8 or j = i + 9 or j = i + 10 or j = i + 11 or j = i + 12 or j = i + 13 or j = i + 14 or j = i + 15 ) ) )

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

case 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 )

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 ) by Lmseg8, A0; :: thesis: verum

end;

case A2: j > i + 7 ; :: thesis: ( j = i + 8 or j = i + 9 or j = i + 10 or j = i + 11 or j = i + 12 or j = i + 13 or j = i + 14 or j = i + 15 )

(i + 7) + 1 <= j by A2, NAT_1:13;
then ( j = i + 8 or j = (i + 8) + 1 or j = (i + 8) + 2 or j = (i + 8) + 3 or j = (i + 8) + 4 or j = (i + 8) + 5 or j = (i + 8) + 6 or j = (i + 8) + 7 ) by Lmseg8, A0;
hence ( j = i + 8 or j = i + 9 or j = i + 10 or j = i + 11 or j = i + 12 or j = i + 13 or j = i + 14 or j = i + 15 ) ; :: 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 or j = i + 8 or j = i + 9 or j = i + 10 or j = i + 11 or j = i + 12 or j = i + 13 or j = i + 14 or j = i + 15 ) ; :: thesis: verum