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

proof

let m be Nat; :: thesis: ex n being Nat st
( n >= m & n in TriangularNumbers )
set w = Triangle m;
A1: Triangle m is triangular ;
take n = (9 * (Triangle m)) + 1; :: thesis: ( n >= m & n in TriangularNumbers )
A2: Triangle m >= m by Th44;
9 * (Triangle m) >= 1 * (Triangle m) by XREAL_1:64;
then (9 * (Triangle m)) + 1 > Triangle m 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