let l be Nat; :: thesis: ex p being Prime st p > l
reconsider two = 2 as Prime by INT_2:28;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
( ( l = 0 & ex p being Prime st
( p is prime & p > l ) ) or ( l = 1 & ex p being Prime st
( p is prime & p > l ) ) or ( 2 <= l & ex p being Prime st
( p is prime & p > l ) ) )
proof
( l <= 2 implies not not l = 0 & ... & not l = 2 ) ;
per cases then ( l = 0 or l = 1 or 2 <= l ) ;
case A1: l = 0 ; :: thesis: ex p being Prime st
( p is prime & p > l )
take two ; :: thesis: ( two is prime & two > l )
thus ( two is prime & two > l ) by A1; :: thesis: verum
end;
case A2: l = 1 ; :: thesis: ex p being Prime st
( p is prime & p > l )
take two ; :: thesis: ( two is prime & two > l )
thus ( two is prime & two > l ) by A2; :: thesis: verum
end;
case A3: 2 <= l ; :: thesis: ex p being Prime st
( p is prime & p > l )
l <= l ! by Th38;
then 2 <= l ! by A3, XXREAL_0:2;
then 2 + 0 <= (l !) + 1 by XREAL_1:7;
then consider j being Element of NAT such that
A4: j is prime and
A5: j divides (l !) + 1 by INT_2:31;
reconsider j9 = j as Prime by A4;
take j9 ; :: thesis: ( j9 is prime & j9 > l )
A6: j <> 0 by A4, INT_2:def 4;
j <> 1 by A4, INT_2:def 4;
hence ( j9 is prime & j9 > l ) by A5, A6, Th39, Th41; :: thesis: verum
end;
end;
end;
hence ex p being Prime st p > l ; :: thesis: verum