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