:: deftheorem Def3 defines square PYTHTRIP:def 3 :
for n being Number holds
( n is square iff ex m being Nat st n = m ^2 );