let n be 4 _or_greater Nat; :: thesis: ( n is triangular implies not n is prime )
assume n is triangular ; :: thesis: not n is prime
then consider k being Nat such that
A1: n = Triangle k ;
k <> 2 by A1, EC_PF_2:def 1, Th12;
hence not n is prime by A1, Th46; :: thesis: verum