theorem Th45: :: PARTPR_1:45

for D being non empty set
for p being PartialPredicate of D holds PP_or (p,(PP_True D)) = PP_True D