let n be Nat; :: thesis: ( n <> 2 implies not Triangle n is prime )
assume A1: n <> 2 ; :: thesis: not Triangle n is prime
assume A2: Triangle n is prime ; :: thesis: contradiction
then A3: n <> 1 by Th11, INT_2:def 4;
n <> 0 by A2, INT_2:def 4;
then A4: not n is trivial by NAT_2:def 1, A3;

per cases ( n is odd or n is even ) ;

suppose n is odd ; :: thesis: contradiction

then ( n = 1 or n = Triangle n ) by INT_2:def 4, A2, Th41;
hence contradiction by Th45, A4, Th11; :: thesis: verum

end;

suppose n is even ; :: thesis: contradiction

then consider k being Nat such that
A5: n = 2 * k by ABIAN:def 2;
A6: k <> 0 by A2, INT_2:def 4, A5;
A7: Triangle n = (n * (n + 1)) / 2 by Th19
.= k * (n + 1) by A5 ;
then k divides Triangle n by NAT_D:def 3;

per cases then ( k = 1 or k = Triangle n ) by INT_2:def 4, A2;

suppose k = 1 ; :: thesis: contradiction

hence contradiction by A1, A5; :: thesis: verum

end;

suppose A8: k = Triangle n ; :: thesis: contradiction

1 = k / k by A6, XCMPLX_1:60
.= n + 1 by A6, XCMPLX_1:89, A7, A8 ;
then n = 0 ;
hence contradiction by INT_2:def 4, A2; :: thesis: verum

end;

end;

end;

end;