max ((<=6n+1 n) /\ SetPrimes) in (<=6n+1 n) /\ SetPrimes by XXREAL_2:def 8;
then max ((<=6n+1 n) /\ SetPrimes) in SetPrimes by XBOOLE_0:def 4;
hence max ((<=6n+1 n) /\ SetPrimes) is Prime by NEWTON:def 6; :: thesis: verum