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

end;

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