:: deftheorem Def1 defines composite NUMBER02:def 1 :
for n being Integer holds
( n is composite iff ( 2 <= n & not n is prime ) );