let p be Integer; :: thesis: ( p is prime implies not p is square )
assume p is prime ; :: thesis: not p is square
then reconsider p = p as non square Element of NAT by ORDINAL1:def 12;
not p is square ;
hence not p is square ; :: thesis: verum