let x be number ; :: thesis: ( x in SquareNumbers iff x is square )
thus ( x in SquareNumbers implies x is square ) ; :: thesis: ( x is square implies x in SquareNumbers )
assume x is square ; :: thesis: x in SquareNumbers
then consider n being Nat such that
A1: x = n ^2 by PYTHTRIP:def 3;
x = Polygon (4,n) by A1;
hence x in SquareNumbers ; :: thesis: verum