theorem Th57: :: PARTPR_1:57

for D being non empty set holds PP_or ((PP_BottomPred D),(PP_True D)) = PP_True D