let i be Nat; :: thesis: not (ArProg (2,3)) . i is triangular
assume (ArProg (2,3)) . i is triangular ; :: thesis: contradiction
then consider k being Nat such that
A1: (ArProg (2,3)) . i = Triangle k by NUMPOLY1:def 2;

per cases ( ex u being Nat st k = (3 * u) + 1 or ex u being Nat st k = (3 * u) + 2 or ex u being Nat st k = 3 * u ) by NUMBER02:23;

suppose ex u being Nat st k = (3 * u) + 1 ; :: thesis: contradiction

then consider u being Nat such that
E1: k = (3 * u) + 1 ;
3 divides (Triangle ((3 * u) + 1)) - 1 by Not3DividesTriangle;
hence contradiction by LemmaBono, A1, E1; :: thesis: verum

end;

suppose ex u being Nat st k = (3 * u) + 2 ; :: thesis: contradiction

then consider u being Nat such that
D1: k = (3 * u) + 2 ;
thus contradiction by A1, Lemma3ArProg, D1, Divides3Triangle2; :: thesis: verum

end;

suppose ex u being Nat st k = 3 * u ; :: thesis: contradiction

then consider u being Nat such that
C1: k = 3 * u ;
thus contradiction by A1, Lemma3ArProg, C1, Divides3Triangle; :: thesis: verum

end;

end;