let n be Nat; :: thesis:
assume A1: n <> 2 ; :: thesis:
assume A2: Triangle n is prime ; :: thesis:
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;

suppose n is odd ; :: thesis:

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

end;

suppose n is even ; :: thesis:

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 by INT_2:def 4, A2;

suppose k = 1 ; :: thesis:

hence contradiction by A1, A5; :: thesis:

end;

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

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:

end;

end;

end;

end;