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