set X = { i where i is Nat : (ArProg (0,2)) . i is triangular } ;
for m being Nat ex n being Nat st
( n >= m & n in { i where i is Nat : (ArProg (0,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 (0,2)) . i is triangular } )
A3: Triangle (4 * m) is triangular by NUMPOLY1:def 2;
A2: Triangle (4 * m) = ((4 * m) * ((4 * m) + 1)) / 2 by NUMPOLY1:19
.= (2 * m) * ((4 * m) + 1) ;
a4: (ArProg (0,2)) . (m * ((4 * m) + 1)) = 0 + (2 * (m * ((4 * m) + 1))) by ArDefNth;
(4 * m) + 1 >= 1 by NAT_1:12;
then AA: m * ((4 * m) + 1) >= m * 1 by NAT_1:4;
m * ((4 * m) + 1) in { i where i is Nat : (ArProg (0,2)) . i is triangular } by A3, a4, A2;
hence ex n being Nat st
( n >= m & n in { i where i is Nat : (ArProg (0,2)) . i is triangular } ) by AA; :: thesis: verum

end;

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