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