let x be Element of SquareNumbers ; :: thesis: x is square
x in SquareNumbers by SUBSET_1:def 1;
then ex n being Nat st x = Polygon (4,n) ;
hence x is square ; :: thesis: verum