:: deftheorem defines BOOL ORDERS_1:def 3 :
for D being set holds BOOL D = (bool D) \ {{}};