let i, j be Nat; :: thesis: ( i <= j & j <= i + 23 & 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 & not j = i + 15 & not j = i + 16 & not j = i + 17 & not j = i + 18 & not j = i + 19 & not j = i + 20 & not j = i + 21 & not j = i + 22 implies j = i + 23 )
assume A0: ( i <= j & j <= i + 23 ) ; :: 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 or j = i + 16 or j = i + 17 or j = i + 18 or j = i + 19 or j = i + 20 or j = i + 21 or j = i + 22 or j = i + 23 )

now :: thesis: ( ( j <= i + 15 & ( 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 ) ) or ( j > i + 15 & ( j = i + 16 or j = i + 17 or j = i + 18 or j = i + 19 or j = i + 20 or j = i + 21 or j = i + 22 or j = i + 23 ) ) )

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

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

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

end;

case A2: j > i + 15 ; :: thesis: ( j = i + 16 or j = i + 17 or j = i + 18 or j = i + 19 or j = i + 20 or j = i + 21 or j = i + 22 or j = i + 23 )

(i + 15) + 1 <= j by A2, NAT_1:13;
then ( j = i + 16 or j = (i + 16) + 1 or j = (i + 16) + 2 or j = (i + 16) + 3 or j = (i + 16) + 4 or j = (i + 16) + 5 or j = (i + 16) + 6 or j = (i + 16) + 7 ) by Lmseg8, A0;
hence ( j = i + 16 or j = i + 17 or j = i + 18 or j = i + 19 or j = i + 20 or j = i + 21 or j = i + 22 or j = i + 23 ) ; :: 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 or j = i + 16 or j = i + 17 or j = i + 18 or j = i + 19 or j = i + 20 or j = i + 21 or j = i + 22 or j = i + 23 ) ; :: thesis: verum