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