:: deftheorem defines EmptyMS PBOOLE:def 3 :
for I being set holds EmptyMS I = I --> {};