:: deftheorem defines PP_False PARTPR_1:def 9 :
for D being set holds PP_False D = D --> FALSE;