:: deftheorem defines PPEmpty PARTPR_2:def 9 :
for D being non with_non-empty_elements set holds PPEmpty D = D --> {};