let D be non empty set ; :: thesis: PP_imp ((PP_BottomPred D),(PP_True D)) = PP_True D
thus PP_imp ((PP_BottomPred D),(PP_True D)) = PP_or ((PP_BottomPred D),(PP_True D)) by Th56
.= PP_True D by Th57 ; :: thesis: verum