theorem Th24: :: NUMBER19:24
for p being Prime st p > 5 holds
ex q being Prime st
( p < q & q divides ((p -' 1) !) + 1 )