theorem Th5: :: HILB10_6:5

for n, e being Nat st 2 <= e & ex i being Nat st (((e ^2) * (e * (e + 2))) * ((n + 1) ^2)) + 1 = i ^2 holds
(e - 1) + (e |^ (e -' 2)) <= n