set X = { i where i is Nat : (ArProg (1,2)) . i is triangular } ;
for m being Nat ex n being Nat st
( n >= m & n in { i where i is Nat : (ArProg (1,2)) . i is triangular } )

proof

let m be Nat; :: thesis: ex n being Nat st
( n >= m & n in { i where i is Nat : (ArProg (1,2)) . i is triangular } )
A3: Triangle ((4 * m) + 1) is triangular by NUMPOLY1:def 2;
Triangle ((4 * m) + 1) = (((4 * m) + 1) * (((4 * m) + 1) + 1)) / 2 by NUMPOLY1:19
.= (2 * ((m * (4 * m)) + (3 * m))) + 1 ;
then A4: Triangle ((4 * m) + 1) = (ArProg (1,2)) . ((m * (4 * m)) + (3 * m)) by ArDefNth;
set n = (m * (4 * m)) + (3 * m);
(4 * m) + 3 >= 1 by NAT_1:12;
then a1: m * ((4 * m) + 3) >= m * 1 by NAT_1:4;
(m * (4 * m)) + (3 * m) in { i where i is Nat : (ArProg (1,2)) . i is triangular } by A3, A4;
hence ex n being Nat st
( n >= m & n in { i where i is Nat : (ArProg (1,2)) . i is triangular } ) by a1; :: thesis: verum

end;

hence { i where i is Nat : (ArProg (1,2)) . i is triangular } is infinite by PYTHTRIP:9; :: thesis: verum