:: deftheorem defines %O PARTIT1:def 8 :
for Y being non empty set holds %O Y = {Y};