let m, n be non zero Nat; :: thesis: ( (6 * m) + 1 is prime & (6 * n) + 1 is prime & LP<=6n+1 m = LP<=6n+1 n implies m = n )
assume A1: ( (6 * m) + 1 is prime & (6 * n) + 1 is prime & LP<=6n+1 m = LP<=6n+1 n ) ; :: thesis: m = n
assume m <> n ; :: thesis: contradiction
then ( m < n or n < m ) by XXREAL_0:1;
hence contradiction by A1, Th33; :: thesis: verum