:: deftheorem defines MESSAGES IDEA_1:def 14 :
MESSAGES = NAT * ;