let n be number ; :: thesis: ( n is square implies n is natural )
assume n is square ; :: thesis: n is natural
then ex m being Nat st n = m ^2 by Def3;
hence n is natural ; :: thesis: verum