let D be set ; :: thesis: PP_not (PP_BottomPred D) = PP_BottomPred D
thus dom (PP_not (PP_BottomPred D)) = dom (PP_BottomPred D) by Def2; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (PP_not (PP_BottomPred D)) or (PP_not (PP_BottomPred D)) . b₁ = (PP_BottomPred D) . b₁ )
hence for b₁ being object holds
( not b₁ in dom (PP_not (PP_BottomPred D)) or (PP_not (PP_BottomPred D)) . b₁ = (PP_BottomPred D) . b₁ ) ; :: thesis: verum