let x be object ; :: thesis: for D being non empty set
for p, q being PartialPredicate of D st x in dom q & (PP_or (p,q)) . x = FALSE holds
q . x = FALSE
let D be non empty set ; :: thesis: for p, q being PartialPredicate of D st x in dom q & (PP_or (p,q)) . x = FALSE holds
q . x = FALSE
let p, q be PartialPredicate of D; :: thesis: ( x in dom q & (PP_or (p,q)) . x = FALSE implies q . x = FALSE )
assume ( x in dom q & (PP_or (p,q)) . x = FALSE ) ; :: thesis: q . x = FALSE
then q . x <> TRUE by Def4;
hence q . x = FALSE by Th3; :: thesis: verum