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

proof

let m be Element of NAT ; :: thesis: ex n being Element of NAT st
( n >= m & n in SquareNumbers )
set w = Triangle m;
A3: Triangle m is triangular ;
reconsider n = (8 * (Triangle m)) + 1 as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis: ( n >= m & n in SquareNumbers )
A4: Triangle m >= m by Th44;
8 * (Triangle m) >= 1 * (Triangle m) by XREAL_1:64;
then (8 * (Triangle m)) + 1 > Triangle m by NAT_1:13;
hence n >= m by A4, XXREAL_0:2; :: thesis: n in SquareNumbers
thus n in SquareNumbers by Th71, A3, Th76; :: thesis: verum

end;

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