let n be Nat; :: thesis: ( n is square implies n is perfect_power )
assume n is square ; :: thesis: n is perfect_power
then consider k being Nat such that
A1: n = k ^2 by PYTHTRIP:def 3;
n = k |^ 2 by A1, NEWTON:81;
hence n is perfect_power ; :: thesis: verum