:: deftheorem defines BOOLEAN MARGREL1:def 11 :
BOOLEAN = {0,1};