let p be Prime; :: thesis: ( p > 5 implies ex q being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) )
assume A1: p > 5 ; :: thesis: ex q being Prime st
( p < q & q divides ((p -' 1) !) + 1 )
consider k, m being Nat such that
A2: ( ((p -' 1) !) + 1 = m * (p |^ k) & not p divides m ) by FIELD_15:4;
m >= 1 + 1

proof

A3: m <> 0 by A2;
assume m < 1 + 1 ; :: thesis: contradiction
then ( 1 <= m & m <= 1 ) by A3, NAT_1:13, NAT_1:14;
then m = 1 by XXREAL_0:1;
hence contradiction by Th23, A1, A2; :: thesis: verum

end;

then consider q being Element of NAT such that
A4: ( q is prime & q divides m ) by INT_2:31;
A5: m divides ((p -' 1) !) + 1 by A2;
then A6: q divides ((p -' 1) !) + 1 by A4, INT_2:9;
q > p -' 1

proof

assume q <= p -' 1 ; :: thesis: contradiction
then q divides 1 by A6, INT_2:1, A4, NEWTON:41;
hence contradiction by A4, INT_2:13; :: thesis: verum

end;

then ( q >= (p -' 1) + 1 & (p -' 1) + 1 = (p - 1) + 1 ) by NAT_1:13;
then q > p by A2, A4, XXREAL_0:1;
hence ex q being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) by A5, A4, INT_2:9; :: thesis: verum