let x be object ; :: thesis: for D being non empty set
for p, q being PartialPredicate of D st x in dom p & p . x = TRUE & x in dom q & q . x = FALSE holds
(PP_imp (p,q)) . x = FALSE
let D be non empty set ; :: thesis: for p, q being PartialPredicate of D st x in dom p & p . x = TRUE & x in dom q & q . x = FALSE holds
(PP_imp (p,q)) . x = FALSE
let p, q be PartialPredicate of D; :: thesis: ( x in dom p & p . x = TRUE & x in dom q & q . x = FALSE implies (PP_imp (p,q)) . x = FALSE )
assume that
A1: x in dom p and
A2: p . x = TRUE and
A3: x in dom q and
A4: q . x = FALSE ; :: thesis: (PP_imp (p,q)) . x = FALSE
A5: dom (PP_not p) = dom p by Def2;
(PP_not p) . x = FALSE by A1, A2, Def2;
hence (PP_imp (p,q)) . x = FALSE by A1, A3, A4, A5, Def4; :: thesis: verum