set T = TriangularNumbers ;
for m being Element of NAT ex n being Element of NAT st
( n >= m & n in TriangularNumbers )

proof

let m be Element of NAT ; :: thesis: ex n being Element of NAT st
( n >= m & n in TriangularNumbers )
reconsider w = Triangle m as Nat by TARSKI:1;
A1: w is triangular ;
reconsider n = (9 * w) + 1 as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis: ( n >= m & n in TriangularNumbers )
A2: w >= m by Th44;
9 * w >= 1 * w by XREAL_1:64;
then (9 * w) + 1 > w by NAT_1:13;
hence n >= m by A2, XXREAL_0:2; :: thesis: n in TriangularNumbers
thus n in TriangularNumbers by Th70, A1, Th77; :: thesis: verum

end;

hence not TriangularNumbers is finite by PYTHTRIP:9; :: thesis: verum