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