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