for j, l being Nat st j <> 1 & j <> 0 & j divides (l !) + 1 holds
j > l by Th39, Th41;