let D be set ; :: thesis: PP_not (PP_True D) = PP_False D
PP_not (PP_False D) = PP_True D by Th43;
hence PP_not (PP_True D) = PP_False D ; :: thesis: verum