let x be Nat; :: thesis: ( x is square implies x is 4 -gonal )
assume x is square ; :: thesis: x is 4 -gonal
then consider n being Nat such that
A2: x = n ^2 by PYTHTRIP:def 3;
x = Polygon (4,n) by A2;
hence x is 4 -gonal ; :: thesis: verum