assume a - 1 is square ; :: thesis: contradiction
then reconsider k = a - 1 as square Element of NAT by ORDINAL1:def 12;
not k + 1 is square ;
hence contradiction ; :: thesis: verum