let D be non empty set ; :: thesis: for p being PartialPredicate of D holds PP_imp ((PP_False D),p) = PP_True D
let p be PartialPredicate of D; :: thesis: PP_imp ((PP_False D),p) = PP_True D
PP_not (PP_False D) = PP_True D by Th43;
hence PP_imp ((PP_False D),p) = PP_True D by Th45; :: thesis: verum